((Parametric) timed) model checking

Slides

Slides with holes

• Part 1: model checking (featuring some lecture materials by Laure Petrucci)
• Part 2: timed automata and timed temporal logics
• Part 3: parametric timed automata

Projects

• Subject of the 2019 project for Sokendai lectures (NII, Tokyo, Japan), using Uppaal
• Subject of the 2024 project for P2S students: build your own CTL model checker (in French)

Links

• IMITATOR
• Uppaal
• Tutorial on parametric verification

License

These slides can be reused under the conditions of their respective licenses, in general Creative Commons CC BY-NC-SA 4.0; author: Étienne André.

LaTeX source available on demand for teaching staff (lecturers, professors…).