Tags:
create new tag
view all tags

Formal Methods in Software Development

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

lecturers: Ivano Salvo and Igor Melatti

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

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   probably remote Yes      
2 17/02/2021   probably remote Yes      
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

Timetable

Day From To Where
Monday 16:00 19:00 Aula G50 (RM115)
Wednesday 12:00 14:00 Aula Alfa (RM062)

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

Edit | Attach | Watch | Print version | History: r37 < r36 < r35 < r34 < r33 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r37 - 2020-12-16 - IvanoSalvo






 
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-2021 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback