SITE TITLE

LOGO DIETI

Verifica di sistemi

Titolo insegnamento in inglese: 

System verification

Lingua: Italiano 

Insegnamento: Verifica di sistemi

Anno di corso: II

CFU: 6

SSD: INF/01

Ore di lezione: 48

Semestre: 2

Modulo: Nessuno

Codice:

Obiettivi formativi:

Il corso si propone di fornire le nozioni di base sottostanti il problema della verifica automatica di proprietà di correttezza di sistemi informatici. In particolare, verranno introdotte e studiate le tecniche di Model Checking. I principali obiettivi del corso sono quelli di familiarizzare lo studente con gli strumenti fondamentali per la comprensione e l'utilizzo degli strumenti automatici di verifica, lo studio dei principali algoritmi di verifica automatica, alcune delle più importanti ottimizzazioni ed estensioni delle tecniche di Model Checking in uso nelle realtà produttive coinvolte nello sviluppo di sistemi sia hardware che software, sistemi embedded e safety-critical.

Contenuti:

La parte iniziale del corso riguarderà lo sviluppo dei prerequisiti relativi agli strumenti di base per la modellazione di sistemi e delle loro proprietà di correttezza. In questa fase, verranno richiamati elementi di logica classica e logica modale; automi a stati finiti su parole finite e automi su parole infinite; tecniche di base per la rappresentazione formale di sistemi (macchine a stati finiti) e delle loro proprietà (logiche temporali LTL e CTL). In seguito, verranno descritte le tecniche algoritmiche per la soluzione automatica dei problemi di verifica: Model Checking esplicito per proprietà CTL; Model Checking per proprietà LTL basato su automi; il problema dell'esplosione del spazio degli stati e il Model Checking simbolico basato su OBDD. Verranno, inoltre, impiegati tool di model checking (NuSMV, SPIN) con esempi di utilizzo. Infine, verranno fatti cenni a tecniche avanzate come, ad esempio, tecniche di Model Checking simbolico basato su soddisfacibilità proposizionale e tecniche di astrazione per sistemi a stati finiti e a stati infiniti.

Prerequisiti: Concetti di Algoritmica, Complessità Computazionale, Logica, Algebra, Automi e Linguaggi Formali

Modalità didattiche: 

Lezioni frontali

 

Materiale didattico: 

Libro di testo: E. M. Clarke, O. Grumberg  D. Peled: “Model Checking”

Lucidi utilizzati per le lezioni frontali del corso

Modalità di esame:

L'esame si articola in prova

 

     

 

 

Solo orale

 

 

 

 

 

 

 

 

 

 

In caso di prova scritta i quesiti sono (*)

 

 

 

 

     

 

Altro 

 

Docente: Benerecetti Massimo