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
- Introdução ao model checking
- Modelação de sistemas paralelos: sistemas transição
- Paralelismo e comunicação com álgebras de processos
- Equivalências de sistemas de transição
- Ferramenta: mCRL2 (modelação)
- Lógicas dinâmicas (e relação com equivalências)
- Ferramenta: mCRL2 (verificação)
- Modelos de tempo real
- Ferramenta: Uppaal (modelação)
- Lógicas temporais: linear (LTL) e ramificada (CTL)
- Ferramenta: Uppaal (verificação)
- Introdução a modelos probabilísticos e estocásticos
- Ferramenta: Uppaal (simulações e 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, 1-11)
- 25 Sep ‘25: Syntax and semantics of CCS (slides 2-behaviour, 11-20). Modelling in mCRL2 (slides 3-mCRL2, 1-12).
- …
Literature and Material
Slides
Main book
- Principles of model checking., Christel Baier and Joost-Pieter Katoen; ISBN: 978-0-262-02649-9
Complementary Bibliography
- mCRL2 Tutorial, available from Uppaal’s website
- Uppaal SMC Tutorial, available from Uppaal’s website
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.