| | | corso | | | | |
Metodi per la verifica del software
Codice: | 373AA | Crediti: | 6 | Semestre: | 2 | Sigla: | MVS | |
|
Settore disciplinare: | INF/01 - Informatica |
Docente
Andrea Corradini
Tel. 0502212786Prerequisiti
Nessuno
Obiettivi di apprendimento
Il corso ha lo scopo di presentare i principi fondamentali della tecnica di verifica di correttezza di sistemi (software e hardware) chiamata Model Checking, e di analizzare alcuni casi concreti di uso di tale tecnica.
Conoscenze. Gli studenti apprenderanno i fondamenti teorici del Model Checking e prenderanno familiarità con SPIN, un model checker ampiamente diffuso e utilizzato anche per sistemi di livello industriale.
Descrizione
Il corso presenta i fondamenti teorici e alcuni aspetti pratici del Model Checking. Dapprima verranno introdotti gli aspetti fondazionali basati su sistemi di transizioni, logiche temporali, linguaggi e automi, nonché alcuni efficienti algoritmi di verifica. Quindi si analizzeranno alcuni case studies utilizzando il linguaggio di modellazione Promela e il suo uso con il model checker SPIN. Gli studenti saranno guidati in attività di sperimentazione con questi sistemi, che saranno propedeutiche alla realizzazione di un progetto che costituirà parte rilevante della valutazione finale.
English Description
The course will present the theoretical foundations and some practical aspects of Model Checking. Firstly, the foundational aspects will be introduced, based on transition systems, temporal logics, languages and automata, as well as some efficient verification algorithms. Next some case studies will be analysed, exploiting the modelling language Promela and its use with the SPIN model checker. The students will be guided in some experimental activities with these systems, which will pave the way to the development of a project that will be part of the final evaluation.
Indicazioni metodologiche
Gli studenti sono invitati a organizzare il processo di apprendimento in moduli flessibili corrispondenti ai vari argomenti presentati nel corso, posti in sequenza logica. Inoltre essi sono invitati a valutare in corso di erogazione il livello di raggiungimento degli obiettivi utilizzando in modo critico le esercitazioni in aula e le attività di laboratorio.
Programma
- Modellazione di sistemi (harware e software) con sistemi di transizioni
- Modellazione composizionale basata su operatori su sistemi di transizioni
- Proprietà linear time come linguaggi di stringhe infinite
- Proprietà di safety e di liveness
- Fairness di processi
- Model checking con Automi di Büchi
- Model checking di formule di Linear Time Logic
- SPIN e Promela
- Cenni su Computation Tree Logic
- Casi di studio
Bibliografia
- Lucidi del corso
- Christel Baier, Joost Peter Katoen, Principles of Model Checking, MIT Press, 2008
- Mordechai Ben-Ari, Principles of the Spin Model Checker, Springer, 2008
Modalità di esame
Progetto e orale