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 2003

Previous years: [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: Tue 8.45-10.15, Wed 16.15-18 in room TB353 (CS-building), first lecture on Wed 15th of Jan-2003. (Period course, only 1st half of the semester.)

Tutorials: Tue 10.15-11, Wed 18-18:45 in room TB353 (CS-building). (Period course, only 1st half of the semester.)

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.

Lecturer: D.Sc.(Tech.) Keijo Heljanko, office hours Mon 13-14 in room TB334.

Course assistant: Lic.Sc.(Tech.) Timo Latvala.

  • Preliminary program for Spring 2003
  • 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 28.1-2003 at 8:45 .ps.gz .pdf
  • Home exercise 2, deadline 4.2-2003 at 8:45 .ps.gz .pdf
  • Home exercise 3, deadline 11.2-2003 at 8:45 .ps.gz .pdf
  • Home exercise 4, deadline 18.2-2003 at 8:45 .ps.gz .pdf
  • Home exercise 5, deadline 25.2-2003 at 8:45 .ps.gz .pdf
  • Current point standings

  • [TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
    Latest update: 22 December 2003. Keijo Heljanko