Modelling of Concurrent Systems with PROMELA
This course focuses on the modeling of reactive concurrent systems using finite state machines. Finite state machines are used for model checking which is a prominent verification technique that has emerged in the last thirty years. Model checking checks whether a model of a given system (specified using transition systems) satisfies properties such as deadlock freedom, invariants or starvation freedom. SPIN is a model checker used to teach concurrency and is applied in industry. PROMELA is the language used for writing system models in SPIN. The SPIN tool has been used for verifying a broad range of different systems in industry like operating systems, communication systems and railway signaling systems.
- Dozent/in: Ruth Schorr