Introduction and objectives

This course provides an introduction to formal techniques to verify computer systems based on models (model checking).

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). Starting to describe transition systems with functors (slides 2-behaviour, frames 1-6).

Literature and Material

Slides

1. Introduction to the course
2. Transition systems and CCS

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.