Introduction and objectives
This course provides an introduction to formal techniques to verify computer systems based on models (model checking).
The official plan of this course is hosted in FCUP here.
Learning outcomes and competences
Students should:
- understand the importance of using logic and formal methods in the development of complex computer systems; and
- be able to model simple systems and specify properties using temporal logics.
Syllabus
- Introduction to model checking
- Modelling of parallel systems: transition systems
- Parallelism and communication with process algebra
- Equivalence of transition systems
- Tool: mCRL2 (modelling)
- Dynamic logics (and relation with equivalences)
- Tool: mCRL2 (verification)
- Real-Timed models
- Tool: Uppaal (modelling)
- Temporal logics: linear (LTL) and branching (CTL)
- Tool: Uppaal (verification)
- Introduction to probabilistic and stochastic models
- Tool: Uppaal (simulations an PLTL)
Lectures
- 18 Sep ‘25: Overview of the module and introduction to model checking (Slides 1-intro.pdf). Transition systems with functors; syntax of sequential process algebra (slides 2-behaviour, frames 1-11)
- 25 Sep ‘25: Syntax and semantics of CCS (slides 2-behaviour, 11-20). Modelling in mCRL2 (slides 3-mCRL2, 1-12). Starting the tutorial “hands-on” with mCRL2.
- 2 Oct ‘25: No lesson due to an ongoing scientific event.
- 9 Oct ‘25: Continuing the tutorial “hands-on” with mCRL2. Equivalence of transition systems (slides 2-behaviour, frames 13-38).
- 16 Oct ‘25: Modal logics (slides 4-modal-logic.pdf. Exercises: specifying and explaining concrete formulas in process logic; (slides 4-modal-logic.pdf, frames 1-22).
- 23 Oct ‘25: More exercises on process logic; process logic with regular expressions (slides 4-modal-logic.pdf, frames 22-26). Modal logic in mCRL2 (slides 3-mCRL2); Process logic vs. bisimulations (slides 4-modal-logic.pdf, frames 28-33).
- 6 Nov ‘25: Frame definability (slides 4-modal-logic.pdf, frames 34-35); LTL and CTL as extensions to modal logic (slides 4-modal-logic.pdf, frames 36-40) - NO Hybrid logic. Timed automata: introduction, syntax, and composition (slides 5-TA-modelling.pdf, frames 1-18).
- 13 Nov ‘25: Timed automata and its composition, exercises; Semantics of Timed Automata, formally (slides 5-TA-modelling.pdf, frames 17-27). Timelocks and zeno paths (slides 5-TA-modelling.pdf, frames 28-40).
Literature and Material
Slides
- Introduction to the course
- Transition systems and CCS
- mCRL2 tool
- Modal logic
- Timed automata: modelling
- Timed automata: verifying
- Stochastic Timed automata
- TBA
Main book
- Principles of model checking., Christel Baier and Joost-Pieter Katoen; ISBN: 978-0-262-02649-9
Extra material
- mCRL2 tutorial exercises
- 1st assignment on mCRL2 - deadline: 9 Nov. 2025
- 2nd assignment on Uppaal - preliminary deadline: 4 Jan. 2026
Complementary Bibliography
- mCRL2 Tutorial, available from mCRL2’s website
- Uppaal SMC Tutorial, available from Uppaal’s website
Previous years
Lecturer
-
-
- José Proença
-
- DCC 1.69
- jose.proenca(at)fc.up.pt
- meet: thu afternoon (email before)
Edit the content of this page here.