FormalMethodsInSoftwareDevelopment20212022 < MFS

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

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

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

---+++ 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==).<br />
There, you can find also the Meet address to follow lessons on-line.

<!--
---+++ Announcement
---+++ In order to receive the registration of the lessons, please subscribe at [[http://151.100.17.205/iscrizione/corso_eng.php?id_corso=13][this link]].
-->

<!--
*2/5/2020*<br />
Lessons will start on *monday, October 5th*. <br />
Interested students that have not received an e-mail containg information of on-line Zoom meetings can contact lecturers via e-mail.
-->

<!--
---+++ As from our Faculty communication, lessons will start on the [[https://web.uniroma1.it/i3s/node/9341][5th October]]
-->

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

---+++ Index

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

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

---+++ 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 [[https://stud.infostud.uniroma1.it/Sest/Log/][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 [[http://www.imm.dtu.dk/~albl/promela.html][this page]] and the corresponding Promela models are [[http://www.imm.dtu.dk/~albl/promela-models.zip][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.

<!--
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  |  05/10/2020  | [[%ATTACHURL%/lesson-01-Salvo.pdf][lesson 1-S]] | Salvo: Introduction to Formal Methods and Model Checking. Modeling concurrent systems.  | |
|  2  |  07/10/2020  | [[%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  |  12/10/2020  | [[%ATTACHURL%/lesson-02-Salvo.pdf][lesson 2-S]] | Salvo: Defining specifications, CTL* syntax and semantics. LTL and Linear Time properties. | |
|  4  |  14/10/2020  | [[%ATTACHURL%/lesson-02-Melatti.pdf][lesson 2-M]]  | Melatti: Murphi example models and relationship with Kriepke structures | |
|  5  |  19/10/2020  | [[%ATTACHURL%/lesson-03-Salvo.pdf][lesson 3-S]] | Salvo: CTL. LTL vs CTL. CTL, LTL and CTL* model checking. | |
|  6  |  21/10/2020  | [[%ATTACHURL%/lesson-03-Melatti.pdf][lesson 3-M]]  | Melatti: Murphi algorithm | Updated: 28/10/2020 |
|  7  |  26/10/2020  | [[%ATTACHURL%/lesson-04-Salvo.pdf][lesson 4-S]] | Salvo: Model checking and automata: regular and \omega-regular properties. On-the-fly LTL model checking. | |
|  8  |  28/10/2020  | [[%ATTACHURL%/lesson-04-Melatti.pdf][lesson 4-M]] [[https://spinroot.com/spin/Doc/SpinTutorial.pdf][slides on Promela]] | Melatti: Introduction to SPIN usage  | |
|  9  |  02/11/2020  | [[%ATTACHURL%/lesson-05-Salvo.pdf][lesson 5-S]] | Salvo: The problem of fairness. LTL and CTL model checking with fariness assumptions. | |
|  10  |  04/11/2020  | [[https://spinroot.com/spin/Doc/SpinTutorial.pdf][slides on Promela]] | Melatti: modeling in SPIN  | |
|  11  |  09/11/2020  | [[%ATTACHURL%/lesson-06-Salvo.pdf][lesson 6-S]] | Salvo: OBDDs, Fixpoints, and Symbolic CTL Model Checking.  | |
|  12  |  11/11/2020  | [[%ATTACHURL%/lesson-06-Melatti.pdf][lesson 6-M]] [[%ATTACHURL%/models.tgz][models 6-M]] | Melatti: optimzations for SPIN verification algorithm  | |
|  13  |  16/11/2020  | [[%ATTACHURL%/lesson-07-Salvo.pdf][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  | [[%ATTACHURL%/lesson-08-Salvo.pdf][lesson 8-S]] | Salvo: Counteracting the state explosion problem I: Partial Order Reduction. | |
|  16  |  25/11/2020  | [[%ATTACHURL%/lesson-08-Melatti.pdf][lesson 8-M]] [[%ATTACHURL%/models_8.tgz][promela example and script]] [[%ATTACHURL%/papers_8.tgz][papers about Spin]] | Melatti: SPIN verification algorithm: LTL and optimisations  | |
|  17  |  30/11/2020  | [[%ATTACHURL%/lesson-09-Salvo.pdf][lesson 9-S]] | Salvo: Counteracting the state explosion problem II: bisimulation, simulation and ACTL, and cone of influence | |
|  18  |  02/12/2020  | [[%ATTACHURL%/lesson-09-Melatti.pdf][lesson 9-M]] | Melatti: NuSMV model checker | |
|  19  |  07/12/2020  | [[%ATTACHURL%/lesson-10-Salvo.pdf][lesson 10-S]] | Salvo: Counteracting the state explosion problem III: abstract interpretation and symmetries. | |
|  20  |  09/12/2020  | [[%ATTACHURL%/packet-10-Melatti.tgz][lesson 10-M]] | Melatti: NuSMV model checker | |
|  21  |  14/12/2019  | [[%ATTACHURL%/lesson-11-Salvo.pdf][lesson 11-S]] | Salvo: Probabilistic Model Checking: Markov chains, probabilistic reachability, qualitative properties, PCTL | |
|  22  |  16/12/2020  | [[%ATTACHURL%/esson-11-Melatti.tgz][lesson 11-M]] | Melatti: CBMC and software model checking  | |
-->

---+++ Old Exams
   * [[%ATTACHURL%/200122.pdf][January 22, 2020]]
   * [[%ATTACHURL%/200212.pdf][February 12, 2020]]
   * [[%ATTACHURL%/200430.pdf][A small collection of questions]]

<a name="orario"></a>

---+++ Timetable

| *Day* | *From* | *To* | *Where* |
| Monday | 2pm | 4pm | Aula G50 (RM115) |
| Wednesday | 1pm | 4pm | Aula G0 (RM115) |
<!--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]].-->

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

<!--Aula Alfa is located at via Salaria 113 (ground floor).-->

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