Formal Methods in Software Development

Announcement

For scheduled online exams, it is possible for students which do not have all the required hardware (PC, smartphone, Internet, etc) to ask for a physical workstation to be used in a Sapienza laboratory. To this aim, students must send a motivated email to the segreteria didattica (segr.didattica@diNOSPAM.uniroma1.it).

Index

Exams
Program
TextBooks
Lessons
Timetable
Software

Results

These are the results for the exam of the 12/2/2020. Votes are at most 16; they will be summed up with the results of either the project or the paper discussion. Who is not present in this list, is not sufficient.

Results

These are the results for the exam of the 22/1/2020. Votes are at most 16; they will be summed up with the results of either the project or the paper discussion. Who is not present in this list, is not sufficient.

Exams

It is mandatory to pass a written exam. Once passed such exam, students have to either write a course project or describe a recent scientific paper on the course arguments.

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

To model the Dolev Strong protocol in one of the model checkers seen during lessons

To modify Murphi or SPIN so as to use Bloom filters instead of hash compaction

Implement statistical model checking in Murphi/SPIN/NuSMV

Given a game map (a grid with obstacles and a goal), create a NuSMV model which generates a controller for that game. Follow the definition of "controller" given here (paragraph 4.1)

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	24/09/2019	lesson 1-S	Salvo: Formal methods, introduction to modeling concurrent systems (Aula "B" - Main Campus Sapienza)
2	25/09/2019	lesson 1-M other material	Melatti: Introduction to Murphi usage (Aula "B" - Main Campus Sapienza)
3	01/10/2019	lesson 2-S	Salvo: Defining specifications, CTL* syntax and semantics, Linear Time properties, LTL and LTL model checking (Aula Magna Sociologia)
4	02/10/2019	lesson 2-M	Melatti: Murphi algorithm (Aula Magna Sociologia)
5	08/10/2019	lesson 3-S	Salvo: CTL. LTL vs CTL. CTL model checking. CTL* model checking.
6	09/10/2019	material 3-M	Melatti: Murphi algorithm; Modeling of a complex system (turbogas)
7	15/10/2019	lesson 4-S	Salvo: Model checking and automata: regular and \omega-regular properties. LTL on-the-fly model checking.
8	16/10/2019	lesson 4-M slides on Promela	Melatti: Introduction to SPIN usage
9	22/10/2019	lesson 5-S	Salvo: Counteracting the state explosion problem I: partial order reduction
10	23/10/2019	lesson 5-M SPIN code	Melatti: SPIN verification algorithm
11	29/10/2019	lesson 6-S	Salvo: The problem of Fairness. LTL and CTL model checking with fairness
12	30/10/2019	lesson 6-M models 6-M	Melatti: optimzations for SPIN verification algorithm
13	05/11/2019	lesson 7-S	Salvo: OBDDs, fixpoints, and Symbolic CTL model checking.
	06/11/2019		CANCELLED
14	12/11/2019	lesson 8-S	Salvo: Symbolic CTL model checking with fairness, Symbolic LTL model checking, and mu-calculus.
15	13/11/2019	lesson 7-M models 7-M NuSMV tutorial NuSMV user manual	Melatti: the NusMV model checker
16	19/11/2019	lesson 9-S	Salvo: Counteracting the state explosion problem II: bisimulation, simulation and ACTL, and cone of influence
17	20/11/2019	lesson 8-M models 8-M	Melatti: the NusMV model checker
18	26/11/2019	lesson 10-S	Salvo: Counteracting the state explosion problem III: abstract interpretation and symmetries.
19	27/11/2019	paper	Melatti: Caching and Disk Murphi
	03/12/2019		CANCELLED
20	04/12/2019	paper lesson 10-M	Melatti: FHP-Murphi
21	10/12/2019	lesson 11-S	Salvo: Probabilistic Model Checking I: Markov chains, probabilistic (constrained) reachability, qualitative properties
22	11/12/2019	lesson 11-M	Melatti: CBMC and software model checking
23	17/12/2019	lesson 12-S	Salvo: Probabilistic Model Checking II: PCTL, linear time properties, probabilistic bisimulation.
24	18/12/2019		Melatti: discussions on ongoing students' projects

Timetable

Free Software for the Course

CMurphi

Spin

NuSMV

CBMC

FHP-Murphi

PRISM