T-79.5301 Reactive Systems (4 cr) P
Spring 2008 (Periods III and IV)
Reactive systems can be found in many embedded systems such as
microprocessors, telecommunication systems and data communication
networks. Their central feature is non-terminating behavior and
reaction to stimuli provided by the environment.
The modeling and verification of reactive systems has become
a natural part of the system development cycle in the design of
VLSI circuits. Similar techniques can also be applied, e.g.,
to the design and implementation of data communication
The course covers the basic theory of modeling reactive systems using
automata, specifying requirements on the behavior of such models using
temporal logic, and verifying these properties using model checking
Lectures and Seminars: Tuesdays 16-18 in room B353 (Computer Science
Tutorials: Tuesdays 18-19 (room B353).
B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie,
A. Petit, L. Petrucci, Ph. Schnoebelen, and P. McKenzie:
Systems and Software Verification - Model-Checking
Techniques and Tools. Springer, 1999.
(Chapters 1-2, 6-11)
E. M. Clarke Jr., O. Grumberg, and D. A. Peled: Model Checking.
The MIT Press, 1999. (Chapters 3-4, 9-11)
Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent
Systems - Specification. Springer, 1992.
(Chapters 3.3, 4.2)
To pass the course, you should:
Completing the above tasks will earn you a basic grade of 3.
Earning 70 % (90 %) of the points from the home assignments will raise your
final grade to 4 (5, respectively).
- give three seminar talks (30-40 min / talk), and
- earn at least 50 % of points awarded from three home assignments (15 points / assignment).
Schedule for Spring 2008
Lecture slides (with corrections to the versions distributed on paper)
- Automata and synchronization [PS] [PDF]
- Temporal logics [PS] [PDF]
- Safety properties [PS] [PDF]
- Fairness properties [PS] [PDF]
- Syntactic classification of temporal formulas [PS] [PDF]
- Automata-theoretic model checking [PS] [PDF]
- Translating LTL to Büchi automata [PS] [PDF]
- Model checking with fairness constraints; CTL* model checking [PS] [PDF]
- Partial order reduction for LTL-X [PS] [PDF]
- Partial order reduction: Complexity, heuristics and correctness [PS] [PDF]
Final results of the course (19 May, 2008)
Literature for seminar talks
Reserved topics are denoted by ***.
*** J. Barnat, I. Černá. Distributed breadth-first search LTL model checking. Formal Methods in System Design 29(2):117-134, 2006.
S. Edelkamp, S. Leue, A. Lluch-Lafuente. Partial-order reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology Transfer (STTT) 6(4):277-301.
The seminar talk should cover Sections 1-2 of the paper (pages 277-285).
*** P. Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design 26(2):77-101, 2005.
G. J. Holzmann. State compression techniques. In The Spin Model Checker - Primer and Reference Manual, pp. 198-214. Addison-Wesley, 2003.
Copies of the book are available both in the Computer Science library and
the TKK main library.
G. J. Holzmann, R. Joshi. Model-driven software verification. In Model Checking Software: Proceedings of the 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004, volume 2989 in Lecture Notes in Computer Science, pp. 76-91. Springer, 2004.
*** G. J. Holzmann, M. H. Smith. An automated verification method for distributed systems software based on model extraction. IEEE Transactions on Software Engineering 28(4):364-377, 2002.
Latest update: 19 May 2008.