Metodi per la verifica del software

Andrea Corradini      Tel. 0502212786

Nessuno

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.

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.

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.

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.

• 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

Progetto e orale