FormalMethodsInSoftwareDevelopment20192020 < MFS

Tags: view all tags
<center>
---+ <b>Formal Methods in Software Development<br /></b>

---++ *Master Degree in Computer Science<br />A. A. 2019/2020*
---++ lecturers: Ivano Salvo and Igor Melatti

melatti@di.uniroma1.it, salvo@di.uniroma1.it</center>

---+++ 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@di.uniroma1.it).

<!--
---+++ Announcement
---+++ The lesson to be held on 6th of November will not take place.
-->

<!--
---+++ Announcement
---+++ The second written exam will take place on the 12th of February at the [[http://www.di.uniroma1.it/it/strutture/laboratori][Colossus Lab]] (via Salaria 113), starting from 10:30 AM. The project/papers presentations will take place at the Colossus Lab immediately after the written exam correction.
-->

<!--
---+++ Announcement
---+++ The second exam, initially scheduled for the 7th of February, has been postponed to the 12th of February at the [[Colossus Lab]] (via Salaria 113), starting from 10:30 AM.
-->

---+++ Index

[[#esami_date][Exams]]<br /> [[#programma][Program]]<br /> [[#libri][TextBooks]]<br /> [[#lezioni][Lessons]]<br /> [[#orario][Timetable]]<br /> [[#software][Software]]

<a name="esami_date"></a>

---+++ 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.

| *Matricola* | *Voto* |
| 1643888 | 13 |
| 1746117 | 13 |
| 1614998 | 13 |

---+++ 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.

| *Matricola* | *Vote* |
| 1746117 | 10 |
| 1903114 | 15.5 |
| 1643888 | 8 |
| 1914000 | 13 |

---+++ 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.

| *Session* | *Date* | *Time* | *Where* | *Confirmed* | *Notes* | *Exam Number on Infostud* | *Infostud registration expires on* |
| 1 | 22/01/2020 | 10:00 - 13:00 | Aula 2 (RM018) in Via del Castro Laurenziano 7a | Yes | | 693149 | expired |
| 2 | 12/02/2020 | 10:30 - 13:00 | Colossus Lab | Yes | | 693150 | expired |
| straord1 | 30/04/2020 | 10:00 - 12:00 | Online | Yes | | 711799 | expired |
| 3 | 19/06/2020 | 15:00 - 18:00 | Online | Yes | | 714631 | expired |
| 4 | 14/07/2020 | 09:00 - 12:00 | Online | Yes | | 717213 | expired |
| 5 | 09/09/2020 | 09:00 - 12:00 | Online | Yes | | 719854 | expired |
| straord2 | 29/11/2020 | 09:00 - 10:00 | Online | Yes | | 734734 | expired |
*It is mandatory to sign up in [[https://stud.infostud.uniroma1.it/Sest/Log/][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 [[%ATTACHURL%/DolevStrong.pdf][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 [[http://mclab.di.uniroma1.it/publications/papers/mari/2014/110_Mari_etal2014.pdf][here (paragraph 4.1)]]

<a name="programma"></a>

---+++ 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

<a name="libri"></a>

---+++ Textbooks and links

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

<a name="lezioni"></a>

---+++ Lessons

| *N* | *Data* | *Material* | *Topics* | *Notes* |
|  1  |  24/09/2019  | [[%ATTACHURL%/lesson-01.pdf][lesson 1-S]]  | Salvo: Formal methods, introduction to modeling concurrent systems (Aula "B" - Main Campus Sapienza) | |
|  2  |  25/09/2019  | [[%ATTACHURL%/lesson-melatti-01.pdf][lesson 1-M]] [[%ATTACHURL%/packet-melatti-01.tgz][other material]] | Melatti: Introduction to Murphi usage (Aula "B" - Main Campus Sapienza)  | |
|  3  |  01/10/2019  | [[%ATTACHURL%/lesson-02.pdf][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  | [[%ATTACHURL%/lesson-melatti-02.pdf][lesson 2-M]]  | Melatti: Murphi algorithm (Aula Magna Sociologia) | |
|  5  |  08/10/2019  | [[%ATTACHURL%/lesson-03-salvo.pdf][lesson 3-S]] | Salvo: CTL. LTL vs CTL. CTL model checking. CTL* model checking. | |
|  6  |  09/10/2019  | [[%ATTACHURL%/packet-melatti-03.tgz][material 3-M]]  | Melatti: Murphi algorithm; Modeling of a complex system (turbogas) | |
|  7  |  15/10/2019  | [[%ATTACHURL%/lesson-04-salvo.pdf][lesson 4-S]] | Salvo: Model checking and automata: regular and \omega-regular properties. LTL on-the-fly model checking. | |
|  8  |  16/10/2019  | [[%ATTACHURL%/lesson-melatti-04.pdf][lesson 4-M]] [[https://spinroot.com/spin/Doc/SpinTutorial.pdf][slides on Promela]] | Melatti: Introduction to SPIN usage  | |
|  9  |  22/10/2019  | [[%ATTACHURL%/lesson-05-salvo.pdf][lesson 5-S]] | Salvo: Counteracting the state explosion problem I: partial order reduction | |
|  10  |  23/10/2019  | [[%ATTACHURL%/lesson-melatti-05.pdf][lesson 5-M]] [[%ATTACHURL%/ch13.pdf][SPIN code]] | Melatti: SPIN verification algorithm  | |
|  11  |  29/10/2019  | [[%ATTACHURL%/lesson-06-salvo.pdf][lesson 6-S]] | Salvo: The problem of Fairness. LTL and CTL model checking with fairness | |
|  12  |  30/10/2019  | [[%ATTACHURL%/lesson-melatti-06.pdf][lesson 6-M]] [[%ATTACHURL%/models.tgz][models 6-M]] | Melatti: optimzations for SPIN verification algorithm  | |
|  13  |  05/11/2019  | [[%ATTACHURL%/lesson-07-salvo.pdf][lesson 7-S]] | Salvo: OBDDs, fixpoints, and Symbolic CTL model checking. | |
| |  06/11/2019  | | CANCELLED | |
|  14  |  12/11/2019  | [[%ATTACHURL%/lesson-08-salvo.pdf][lesson 8-S]] | Salvo: Symbolic CTL model checking with fairness, Symbolic LTL model checking, and mu-calculus. | |
|  15  |  13/11/2019  | [[%ATTACHURL%/lesson-melatti-07.pdf][lesson 7-M]] [[%ATTACHURL%/models-07.tgz][models 7-M]] [[%ATTACHURL%/NuSMV.tutorial.pdf][NuSMV tutorial]] [[%ATTACHURL%/NuSMV.userman.pdf][NuSMV user manual]] | Melatti: the NusMV model checker  | |
|  16  |  19/11/2019  | [[%ATTACHURL%/lesson-09-salvo.pdf][lesson 9-S]] | Salvo: Counteracting the state explosion problem II: bisimulation, simulation and ACTL, and cone of influence | |
|  17  |  20/11/2019  | [[%ATTACHURL%/lesson-melatti-08.pdf][lesson 8-M]] [[%ATTACHURL%/models-08.tgz][models 8-M]] | Melatti: the NusMV model checker  | |
|  18  |  26/11/2019  | [[%ATTACHURL%/lesson-10-salvo.pdf][lesson 10-S]] | Salvo: Counteracting the state explosion problem III: abstract interpretation and symmetries. | |
|  19  |  27/11/2019  | [[http://mclab.di.uniroma1.it/publications/papers/papers/Della%20Penna2004a.pdf][paper]] | Melatti: Caching and Disk Murphi  | |
| |  03/12/2019  | | CANCELLED | |
|  20  |  04/12/2019  | [[http://mclab.di.uniroma1.it/publications/papers/papers/Della%20Penna2006a.pdf][paper]] [[%ATTACHURL%/fhpmurphi.pdf][lesson 10-M]] | Melatti: FHP-Murphi  | |
|  21  |  10/12/2019  | [[%ATTACHURL%/lesson-11-salvo.pdf][lesson 11-S]] | Salvo: Probabilistic Model Checking I: Markov chains, probabilistic (constrained) reachability, qualitative properties | |
|  22  |  11/12/2019  | [[%ATTACHURL%/lesson-melatti-10.tgz][lesson 11-M]] | Melatti: CBMC and software model checking  | |
|  23  |  17/12/2019  | [[%ATTACHURL%/lesson-12.pdf][lesson 12-S]] | Salvo: Probabilistic Model Checking II: PCTL, linear time properties, probabilistic bisimulation.  | |
|  24  |  18/12/2019  | | Melatti: discussions on ongoing students' projects  | |
<a name="orario"></a>

---+++ Timetable

| *Day* | *From* | *To* | *Where* |
| Tuesday | 14:00 | 17:00 | Aula 2 (RM018) in Via del Castro Laurenziano 7a |
| Wednesday | 14:00 | 16:00 | Aula 2 (RM018) in Via del Castro Laurenziano 7a |
<!--L'aula informatica 15 si trova [[http://www.studiareinformatica.uniroma1.it/Test-aula#smart_aula_deffa19a-65db-4abe-be55-4178b791dc1b][all'interno del Laboratorio "Paolo Ercoli" di via Tiburtina]].-->
<!--The first and second lessons (24th and 25th of September 2019) will take place in Aula "B" -  Main Campus Sapienza - Aule SCIENZE BIOCHIMICHE (CU010-E01P01L001).

The detailed Map of the Main Campus Sapienza can be viewed [[https://www.uniroma1.it/sites/default/files/PIANTA_LEGENDA_DEF_1.pdf][here]].-->

<a name="software"></a>

---+++ Free Software for the Course

[[http://mclab.di.uniroma1.it/site/index.php/software/18-cmurphi][CMurphi]]

[[http://spinroot.com/spin/whatispin.html][Spin]]

[[http://nusmv.fbk.eu/][NuSMV]]

[[https://www.cprover.org/cbmc/][CBMC]]

[[http://mclab.di.uniroma1.it/site/index.php/software/17-fhp-murphi][FHP-Murphi]]

[[https://www.prismmodelchecker.org/][PRISM]]