Introduction to Discrete-Systems Theory
Synopsys
Discrete-state systems are the systems whose state evolves via a sequence of discrete, instantaneous state-changes. Examples of discrete-state systems are hardware systems, embedded software systems, mixed hardware-software systems, as well as general software systems. Examples of systems which are not discrete-state include many systems studied in physics and mechanics, whose state evolves in a continuous fashion in time, as well as physical systems with their digital control.
The course provides an introduction to the modeling, specification, verification and analysis of discrete-state systems. The course will emphasize applications to hardware systems and embedded software systems, and will introduce concepts that can be used to reason on general software systems.
The Basics
Instructor: Luca de Alfaro]
Email: my_first_name@soe.ucsc.edu
Location: 10:00-11:45, TTh, Porter Acad 246
Office Hours: Tuesdays, 1-2pm, or by appointment (email the instructor)
Textbook: We will use various material available on the web; all reading resources will be available at this web page.
Reading Material
Lecture Notes
Other readings
Notes on BDDs, from a class taught at EPFL by Tom Henzinger.
Papers on MiniSat, the SAT-solver.
Three-valued abstraction paper, describing the refinement method described in class.
Temporal Safety Proofs for Systems Code, the paper on BLAST described in class.
Kernighan's Trojan Horse (highly recommended reading).
Homework
- Homework 1, due Thursday October 4: Problem 2, page 8.
- Homework 2, due Thursday October 11: Problems 3 and 4, page 10.
Homework 3, on implementation of BDD operations, due Thursday October 25.
Homework 4, the traffic light example.
Homework 5, verification of the traffic light example.