Formal Methods in Software Development

Announcements

17/9/2021: Lessons will start on Wednesday, September 22nd, room G0, viale Regina Elena 295.

Students are invited to join the Classroom FMSD, code: w6zmvie (use your Sapienza account @studenti.uniroma1.it).
There, you can find also the Meet address to follow lessons on-line.

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.

It is mandatory to sign up in infostud.

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

Old Exams

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

Timetable

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

Free Software for the Course

CMurphi

Spin

NuSMV

CBMC

FHP-Murphi

PRISM