Metodi per la Verifica Automatica dei Sistemi
Secondo Semestre 2009-10

Docenti:

Salvatore La Torre

Margherita Napoli

Domenico Parente

Lezioni: n.d.

Ricevimento Studenti:   orario

Avvisi

• 25/1/2010:
  Gli studenti interessati a seguire il corso sono invitati a contattare il prof. La Torre oppure il prof. Parente via email.

Esami

L'esame consiste nello svolgimento degli esercizi dati durante il corso, nella presentazione di un seminario di approfondimento su uno degli argomenti avanzati introdotti al corso ed in un colloquio finale.

Programma del corso

PARTE A: Model-checking di sistemi a stati finiti.

• Modellazione di sistemi: Automi
• Specifiche di sistemi: Logica Temporale
  • Logica lineare: LTL
  • Logica branching-time: CTL e CTL*
  • Logica temporale graded
• Model checking
  • CTL model checking
  • Automi su oggetti infiniti: Buchi, Rabin, Muller, Parity
  • LTL model checking
  • Graded model checking
  • Il problema della esplosione del numero degli stati
• Fairness
  • Strutture di Kripke con fairness
  • Fair CTL
  
  
• Model checking simbolico
  • Computazione simbolica dell'insieme degli stati per CTL e Fair CTL
  • Approccio simbolico per LTL
  • Approccio simbolico per logiche graded
  • Diagrammi di decisione binaria (BDD)
  • Rappresentazione di automi con BDD
  • Model checking basato sui BDD
  • Tool: Graded-CTL NuSMV

PARTE B: Model-checking di programmi.

• Modelli di programmi sequenziali
  • Automi push-down (PDA)
  • Modellazione di programmi: macchine ricorsive a stati finiti (RSM)
  • Programmi Booleani
• Model-checking di programmi sequenziali
  • PDA raggiungibilità e giochi
  • Model checking di RSM
  • Logica temporale CARET
• Programmi concorrenti e parametrici
  • Automi push-down multistack
  • Programmi Booleani concorrenti
  • Programmi Booleani parametrici
  • Interfacce lineari
  • Raggiungibilita'
  • Coversione da programmi concorrenti/parametrici a programmi sequenziali
• Implementazione di model-checkers simbolici
  • Fixed-point calculus
  • Un semplice algoritmo per programmi Booleani
  • Algoritmi entry-forward e entry-forward ottimizzato
  • Algoritmo di raggiungibilita' per programmi concorrenti entro un numero fissato di context-switches
  • Algoritmo di raggiungibilita' per programmi parametrici entro un numero fissato di round-robin
  • Tool:Getafix

PARTE C: Sistemi real-time e con costanti parametriche.

• Modelli quantitativi
  • Automi temporizzati
  • Automi temporizzati con costanti parametriche
  • Automi ibridi
• Specifiche real-time e parametriche
  • Logiche temporali real-time: TCTL e MITL
  • Logiche temporali discrete con parametri: PLTL e PCTL
  • Logiche temporali real-time parametriche: PMITL e PTCTL

Testi

• B.Berard, M.Bidoit, A.Finkel, F.Laroussinie, A.Petit, L.Petrucci, Ph.Schnoebelen, P.McKenzie, "System and Software Verification: Model-checking Tecniques and Tools", Springer.
• E.Clarke, O.Grumberg, D.Peled, "Model-checking", MIT press.