campUAS

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.