Formal Methods in Software Development

Announcement

In order to receive the registration of the lessons, please subscribe at this link.

Index

Exams
Program
TextBooks
Lessons
Tietable
Software

Exams

It is mandatory to pass a written exam (note: for remote exams, it is possible that an equivalent oral exam will be performed instead). Once passed such exam, students have to either write a course project or describe a recent scientific paper on the course arguments.

Session	Date	Time	Where	Confirmed	Notes	Exam Number on Infostud	Infostud registration expires on
1	27/01/2021	4pm	remote	Yes	public gmeet room	739258	26/01/2021
2	17/02/2021		probably remote	Yes		739259	16/02/2021
straord1	approx 04/2021
3	approx 06/2021
4	approx 07/2021
5	approx 09/2021
straord2	approx. 11/2021

It is mandatory to sign up in infostud by selecting, for the desired session, the exam number shown in the last-but-one column above.

For online exams, instructions will be sent by email to registered-on-Infostud students only

Projects

Consider the industrial case studies which have been verified using SPIN; they are listed in this page and the corresponding Promela models are these.

Pick one of the above models and translate it into an equivalent Murphi model and into an equivalent NuSMV model.

Then write a presentation containing:

1) a brief explanation of the case study (the page above also list the main paper of each case study);

2) a description (as formal, i.e., generic, as possible) of how the translation has been performed;

3) a discussion of the results obtained by running the verification with all 3 model checkers.

The presentation will have to be discussed during an exam session (provided that the first common part of the exam has been passed). It must fit in 20 minutes; however, it must also include (as extra material) full details in case the lecturers ask for them.

Program of the Course

Modelling of Discrete Systems: Kripke structures.

Temporal Logics: CTL, LTL, CTL*

Formal verification that a system satisfy a specification: Model Checking Problem, computational complexity and classical solutions.

Main solutions to the Model Checking problem:

• explicit: Buchi automata, on-the-fly computation, state space reduction (symmetric reduction and partial order reduction)
• symbolic: mu-calculus, OBDD.

Compositional Reasoning

Software Model Checking

Bounded Model Checking

Probabilistic Model Checking

Using Model Checkers for HW/SW systems verification:

• Explicit model checkers: SPIN and Murphi
• Symbolic bounded and unbounded model checker: NuSMV
• Software model checkers: CBMC
• Probabilistic model checkers: FHP-Murphi and PRISM

For each model checker, the following will be discussed:

• input language
• execution model
• logic for properties specification
• implementation techniques

Textbooks and links

"Model Checking, Second Edition", di Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith, 2018

Lessons

N	Data	Material	Topics	Notes
1	05/10/2020	lesson 1-S	Salvo: Introduction to Formal Methods and Model Checking. Modeling concurrent systems.
2	07/10/2020	lesson 1-M other material	Melatti: Introduction to Murphi usage (Aula "B" - Main Campus Sapienza)
3	12/10/2020	lesson 2-S	Salvo: Defining specifications, CTL* syntax and semantics. LTL and Linear Time properties.
4	14/10/2020	lesson 2-M	Melatti: Murphi example models and relationship with Kriepke structures
5	19/10/2020	lesson 3-S	Salvo: CTL. LTL vs CTL. CTL, LTL and CTL* model checking.
6	21/10/2020	lesson 3-M	Melatti: Murphi algorithm	Updated: 28/10/2020
7	26/10/2020	lesson 4-S	Salvo: Model checking and automata: regular and \omega-regular properties. On-the-fly LTL model checking.
8	28/10/2020	lesson 4-M slides on Promela	Melatti: Introduction to SPIN usage
9	02/11/2020	lesson 5-S	Salvo: The problem of fairness. LTL and CTL model checking with fariness assumptions.
10	04/11/2020	slides on Promela	Melatti: modeling in SPIN
11	09/11/2020	lesson 6-S	Salvo: OBDDs, Fixpoints, and Symbolic CTL Model Checking.
12	11/11/2020	lesson 6-M models 6-M	Melatti: optimzations for SPIN verification algorithm
13	16/11/2020	lesson 7-S	Salvo: Symbolic CTL model checking with fairness, Symbolic LTL model checking, and mu-calculus.
14	18/11/2020	see lesson 12	Melatti: optimzations for SPIN verification algorithm
15	23/11/2020	lesson 8-S	Salvo: Counteracting the state explosion problem I: Partial Order Reduction.
16	25/11/2020	lesson 8-M promela example and script papers about Spin	Melatti: SPIN verification algorithm: LTL and optimisations
17	30/11/2020	lesson 9-S	Salvo: Counteracting the state explosion problem II: bisimulation, simulation and ACTL, and cone of influence
18	02/12/2020	lesson 9-M	Melatti: NuSMV model checker
19	07/12/2020	lesson 10-S	Salvo: Counteracting the state explosion problem III: abstract interpretation and symmetries.
20	09/12/2020	lesson 10-M	Melatti: NuSMV model checker
21	14/12/2019	lesson 11-S	Salvo: Probabilistic Model Checking: Markov chains, probabilistic reachability, qualitative properties, PCTL
22	16/12/2020	lesson 11-M	Melatti: CBMC and software model checking

Old Exams

• January 22, 2020
• February 12, 202o
• A small collection of questions

Timetable

Aula G50 is located at Palazzina G V.le Regina Elena 295 (third floor).

Aula Alfa is located at via Salaria 113 (ground floor).

Free Software for the Course

CMurphi

Spin

NuSMV

CBMC

FHP-Murphi

PRISM

• lesson-11-Salvo.pdf: lesson-11-Salvo.pdf