TCS / Studies / T-79.186 Reactive Systems
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.186 Reactive Systems (2 cr) P

Spring 2004

Previous years: [Spring 2003] [Spring 2002] [Spring 2001] [Spring 2000] [Spring 1999]

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 stimulus provided by the environment.

The modeling and verification of reactive systems has become a natural part of system development cycle in the design of VLSI circuits. Similar techniques can also be applied, e.g., to assist the design and implementation of data communication protocols.

The 1997 "Nobel prize of computer science", the A. M. Turing award, was given to Amir Pnueli, a pioneer of verification of reactive systems:

"It is time that formal verification (of both software and hardware systems) be demoted from an art practiced by the enlightened few to an activity routinely and mundanely performed by a cadre of Verification Engineers (a new profession), as a standard part of the system development process."

The contents of the course include the modeling of reactive systems, specification of properties using temporal logic, and the verification of such properties. In addition, basics of model checking algorithms are introduced, and their underlying theory is explored.

Requirements: Seminar talks and home exercises.

Lectures: Wed 16.15-18 in room TB353 (CS-building), first lecture on Wed 14th of Jan.

Tutorials: Wed 18-18:45 in room TB353 (CS-building).

Literature: 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, 190 p., Springer 1999, (Chapters 1-2, 6-11).

E.M. Clarke, O. Grumberg, and D.A. Peled: Model Checking, 314 p., MIT Press 1999, (Chapters 3, 9-13).

In addition scientific articles.

Lectures and tutorials: Lic.Sc.(Tech.) Timo Latvala.

  • Preliminary program for Spring 2004
  • Lecture 1 .ps.gz .pdf
  • Lecture 2 .ps.gz .pdf
  • Lecture 3 .ps.gz .pdf
  • Lecture 4 .ps.gz .pdf
  • Lecture 5 .ps.gz .pdf
  • Lecture 6 .ps.gz .pdf
  • Lecture 7 .ps.gz .pdf
  • Lecture 8 .ps.gz .pdf
  • Lecture 9 .ps.gz .pdf
  • Lecture 10 .ps.gz .pdf
  • Lecture 11 .ps.gz .pdf
  • Home exercise 1, deadline 4.2.2004 at 16:15 .ps.gz .pdf
  • Home exercise 2, deadline 18.2.2004 at 16:15 .ps.gz .pdf
  • Home exercise 3, deadline 3.3.2004 at 16:15 .ps.gz .pdf
  • Home exercise 4, deadline 17.3.2004 at 16:15 .ps.gz .pdf
  • Home exercise 5, deadline 31.3.2004 at 16:15 .ps.gz .pdf
  • Bonus home exercise, deadline 28.4.2004 at 16:15 .ps.gz .pdf
  • Current point standings

  • [TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
    Latest update: 23 December 2004. Timo Latvala