
T79.5301 Reactive Systems (4 cr) P
Spring 2008 (Periods III and IV)
Previous years:
[Spring 2007]
[Spring 2006]
Reactive systems can be found in many embedded systems such as
microprocessors, telecommunication systems and data communication
networks. Their central feature is nonterminating 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
protocols.
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
algorithms.
Course coordinator:
Heikki Tauriainen.
Lectures and Seminars: Tuesdays 1618 in room B353 (Computer Science
building).
Tutorials: Tuesdays 1819 (room B353).
Literature:

B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie,
A. Petit, L. Petrucci, Ph. Schnoebelen, and P. McKenzie:
Systems and Software Verification  ModelChecking
Techniques and Tools. Springer, 1999.
(Chapters 12, 611)

E. M. Clarke Jr., O. Grumberg, and D. A. Peled: Model Checking.
The MIT Press, 1999. (Chapters 34, 911)

Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent
Systems  Specification. Springer, 1992.
(Chapters 3.3, 4.2)

Scientific articles.
To pass the course, you should:
 give three seminar talks (3040 min / talk), and
 earn at least 50 % of points awarded from three home assignments (15 points / assignment).
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).
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]
 Automatatheoretic 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]
Home assignments
Final results of the course (19 May, 2008)
Literature for seminar talks
Reserved topics are denoted by ***.

*** J. Barnat, I. Černá. Distributed breadthfirst search LTL model checking. Formal Methods in System Design 29(2):117134, 2006.

S. Edelkamp, S. Leue, A. LluchLafuente. Partialorder reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology Transfer (STTT) 6(4):277301.
The seminar talk should cover Sections 12 of the paper (pages 277285).

*** P. Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design 26(2):77101, 2005.

G. J. Holzmann. State compression techniques. In The Spin Model Checker  Primer and Reference Manual, pp. 198214. AddisonWesley, 2003.
Copies of the book are available both in the Computer Science library and
the TKK main library.

G. J. Holzmann, R. Joshi. Modeldriven software verification. In Model Checking Software: Proceedings of the 11th International SPIN Workshop, Barcelona, Spain, April 13, 2004, volume 2989 in Lecture Notes in Computer Science, pp. 7691. 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):364377, 2002.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 19 May 2008.
