elenco    
        corso    

Metodi per la verifica del software

Codice: 373AACrediti: 6Semestre: 2Sigla: MVS 
 
Settore disciplinare: INF/01 - Informatica

Docente

Andrea Corradini   andrea@di.unipi.it  Stanza 357  Tel. 0502212786

Prerequisiti

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

     

Bibliografia

Modalità di esame

Progetto e orale

Ulteriore pagina web del corso: http://didawiki.cli.di.unipi.it/doku.php/magistraleinformatica/mvs/start


home


email