Course content
The aim of this module is to introduce key concepts related to the formal verification of concurrent and distributed systems.
This module presents the basis of two approaches for verification: Model Checking and Petri Nets. The following aspects are addressed:
- Introduction and role of verification in the development process.
- Kripke structures for modeling systems.
- Temporal logics (LTL and CTL) for expressing verifiable properties.
- Model Checking verification: solving LTL model checking via Buchi Automata.
- Model Checking verification: solving CTL model checking via Labeling procedure.
- Petri Nets, modeling of concurrency, basic properties.
- Verification of behavioral properties and invariants.
