Formal Methods in Software Development

Master Degree in Computer Science
A. A. 2021/2022

lecturers: Ivano Salvo and Igor Melatti

melatti@diNOSPAM.uniroma1.it, salvo@di.uniroma1.it

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.

Session Date Time Where Notes
1 approx 01/2022      
2 approx 02/2022      
straord1 approx 04/2022      
3 approx 06/2022      
4 approx 07/2022      
5 approx 09/2022      
straord2 approx. 11/2022      
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

N Data Material Topics Notes

Old Exams

Timetable

Day From To Where
Monday 2pm 4pm Aula G50 (RM115)
Wednesday 1pm 4pm Aula G0 (RM115)

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

Edit | Attach | Watch | Print version | History: r4 < r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r4 - 2021-12-13 - IgorMelatti






 
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
Torna al Dipartimento di Informatica
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback