Metodi di verifica di sistemi

Docente: Benedetto Intrigila

Comunicazioni


Lezioni


Materiale didattico

Informazioni

Anno accademico2024-2025
Crediti6
SettoreINF/01
Anno2
Semestre1
PropedeuticitàNessuna

Programma

Model checking. Approccio esplicito e simbolico.

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

Inviare una mail per prendere un appuntamento


Modalità di esame

Progetto (da fare in gruppo) in cui verrà usato un tool di model checking su un sistema semplice.

Prova orale di verifica (individuale) sugli aspetti essenziali della parte teorica.