Il model checking è una tecnica per la verifica di proprietà di sistemi che possono essere rappresentati come macchine a stati finiti. E' in grado di produrre (in determinate condizioni) dei certificati formali che garantiscono che il sistema ha la proprietà richiesta.
Nella parte avanzata del corso verra' considerato
l'uso del model checking nel planning e/o per i sistemi ibridi (con variabili discrete e continue).
Testi di riferimento
Systems and Software Verification
Model-Checking Techniques and Tools
Autori: Berard, B., Bidoit, M., Finkel, A., Laroussinie, F.,
Petit, A., Petrucci, L., Schnoebelen, P
Ricevimento studenti
Per appuntamento
Modalità di esame
Progetto, in cui verrà usato un tool di model checking su un sistema semplice.
Prova orale di verifica sugli aspetti essenziali della parte teorica.