22926 Models and Specification Methods for Concurrent and Reactive Systems 1

Credits: 4 graduate credits in Computer Science

Prerequisite: Admission to the graduate program in Computer Science 2

The course is based on a reader edited by Mark Trakhtenbrot.

The course presents a variety of approaches (algebraic and visual) for specification and analysis of concurrent communicating systems, compares these approaches and presents their principles within a uniform framework. Students are acquainted with the motivation, concepts and specification methods that enable programmers of such systems to precisely describe, represent and validate them. The course, which is for the most part theoretical, also provides an opening to applications through a series of appropriate examples, and the use of programming tools that implement the various approaches covered and give students practical experience in formal specification and analysis of systems.

Topics: Processes, equivalences, operators – labeled transitions systems (LTS), equivalences for LTS, operators and their characteristics (serial operators, various kinds of parallel assemblies); Process calculations – basic calculus communicating systems (CCS), LOTOS specification language compared with CCS, value passing mechanisms; Visual formalism – statecharts, Petri nets, Live Sequence Charts.

---

1There is some overlap in the content of this and other courses. For details, see Overlapping Courses.

2Students who have not fulfilled this requirement may, under certain circumstances, enroll in this course.