|
|||||||||||||||||||||||||||||||||||||||||||
|
|
Metodi Formali
Edizione dell'a.a. 2007/08
|
||||||||||||||||||||||||||||||||||||||||||
Home page
| Codice | Descrizione |
|---|---|
| D.III.2 | Diagrammi UML degli stati e delle transizioni |
Esempi di codifica NuSMV di diagrammi degli stati e verifica di loro proprietà
Il bambino e l'interruttore
| Nome | Descrizione |
|---|---|
| Bambino | Un bambino irrequieto guidato da eventi |
| Bambino in stallo | Un bambino irrequieto può andare in stallo? |
| Bambino/interruttore | Un bambino irrequieto che gioca con un interruttore: sistema asincrono composto da due sistemi interagenti ben connessi |
| Bambino/interruttore in stallo | Esistono modi di interconnettere i due componenti che portano il sistema in stallo? |
Un precedente famoso
Altri esempi
| Nome | Descrizione |
|---|---|
| Cliente/Banca | I clienti visti da una banca |
| Docente | Docenti universitari |
Materiale di approfondimento
| Descrizione |
|---|
|
Davide Nifosi. Verifica formale del software: Spin. Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007. |
|
Alfonso Calciano, Federico Covino. Reverse engineering e verifica di proprietà di un sistema Treno+Auto. Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007. |
|
Claudio Corona, Giorgio Camerani. Uno strumento per la verifica automatica di reti digitali. Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007. |
|
Francesco Maria Delle Fave, Valerio Gheri. Modellazione e verifica formale di algoritmi per la mutua esclusione in ambiente distribuito. Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007. |
|
Francesco Cusmai, Marta Monteleone, Silvia Orsi. Spin: comunicazione tra N processi attraverso un unico canale condiviso. Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007. |
Programmi disponibili
| Nome | Descrizione |
|---|---|
| nuSMV | Model checker per logiche temporali (symbolic e bounded model checking) |
| SPIN | Tool di verifica e model checker per logiche temporali (orientato all'analisi di sistemi concorrenti e/o distribuiti) |
Esercizi
| Codice | Descrizione |
|---|---|
| E.III.20060718 | Pneumatici (codice) |
| E.III.20070320 | Modem |
| E.III.20070723 | Noleggio DVD |
| E.III.20090116 | Aperitivi |
[This web site could never be realised without the sophisticated features of a pure text editor and the extreme power of 220V]