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

19 Sep ‘24: Overview of the module and introduction to model checking (Slides 1-intro.pdf). Starting to describe transition systems with functors (slides 2-behaviour, frames 1-6).
24 Sep ‘24: Transition systems with functors; syntax of sequential process algebra (slides 2-behaviour, frames 6-18).
26 Sep ‘24: Syntax and semantics of CCS (slides 2-behaviour, frames 18-29).
1 Oct ‘24: Modelling in mCRL2 (slides 3-mCRL2, frames 1-12).
3 Oct ‘24: No lesson.
8 Oct ‘24: Equivalence of transition systems (slides 2-behaviour, frames 13-38).
10 Oct ‘24: Modal logics (slides 4-modal-logic.pdf, frames 1-24).
15 Oct ‘24: Exercises: specifying and explaining concrete formulas in process logic; process logic with regular expressions (slides 4-modal-logic.pdf, frames 25-31).
17 Oct ‘24: Modal logic in mCRL2 (slides 3-mCRL2; Process logic vs. bisimulations; Richer modal logics (slides 4-modal-logic.pdf, frames 33-47).
22 Oct ‘24: LTL, CTL, and Hybrid logic; Frame definability (slides 4-modal-logic.pdf, frames 47-53). Introduction to timed automata (slides 5-TA-modelling.pdf, frames 1-12).
24 Oct ‘24: Timed automata and its composition, formally; Quick introduction to Uppaal (slides 5-TA-modelling.pdf, frames 12-21).
5 Nov ‘24: Exercises on the composition of Timed Automata; Modelling in Uppaal; Introduction to the semantics of Timed Automata, formally (slides 5-TA-modelling.pdf, frames 21-29).
7 Nov ‘24: Semantics of Timed Automata, formally; Timelocks and zeno paths (slides 5-TA-modelling.pdf, frames 29-38).
12 Nov ‘24: Revision on timelocks and zeno paths; modelling extensions in Uppaal (slides 5-TA-modelling.pdf, frames 36-55).
14 Nov ‘24: Comparing Timed Automata (slides 6-TA-verification.pdf, frames 1-6).
19 Nov ‘24: Timed and untimed bisimulations (slides 6-TA-verification.pdf, frames 6-11)
21 Nov ‘24: CTL in Uppaal (slides 6-TA-verification.pdf, frames 12-25)
26 Nov ‘24: Review CTL in Uppaal; mutual exclusion examples in Uppaal (slides 6-TA-verification.pdf, frames 19-41)
28 Nov ‘24: Probabilistic transition systems (slides 7-mchains.pdf, frames 1-16)
3 Dec ‘24: Probabilities in Uppaal (slides 7-mchains.pdf, frames 16-30)
5 Dec ‘24: EARS approach to requirement engineering 8-ears.pdf, frames 1-38)
10 Dec ‘24: EARS approach - revision and exercises 8-ears.pdf, frames 38-55); Lines of work on verification of interacting (real-time) systems
12 Dec ‘24: Hybrid programming in Lince 9-lince.pdf - syntax and exercises
17 Dec ‘24: Semantics of hybrid programs in Lince; random simulations in Lince 9-lince.pdf

Literature and Material

Slides

Main book

Principles of model checking., Christel Baier and Joost-Pieter Katoen; ISBN: 978-0-262-02649-9

Extra material

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.