Introduzione
al
corso: Finalità del corso. Caratteristiche, vantaggi e
limiti dei Metodi Formali. Dal concetto di FSM a quello di ASM e di
Automa di Kripke.
Introduzione alle Abstract
State Machines (vedi paragrafo 2.4 del
testo 1.) : concetti di struttura algebrica e di aggiornamento di
funzioni
Costruttori
per
regole
di
transizione, il concetto di Riserva
ed aggiornamento di domini, il concetto di locazione ed aggiornamneto
di locazione, aggiornamenti inconsistenti. Esempi di specifiche ASM:
Advanced Clock (2 versioni), Safety Injection System, One way traffic
light control system, Sluice Gate System, Fattoriale, Ordinamento di un
vettore. Questo
documento contiene i requisiti del Safety Injection
System. Questo
documento presenta i casi del One way traffic
light control system e Sluice Gate System.
AsmetaL,
un linguaggio per la codifica di specifiche
ASM. A
user-guide
per AsmetaL. AsmetaL è disponibile a
http://asmeta.sourceforge.net/userdoc/language.html
Attività
di
laboratorio su validazione tramite scenari. Esempi.
Soluzioni.
Composizione
di
modelli:
ASM multi agenti. Esempi del
Sluice
Gate
System
ad
agenti (in
examples\sluicegate) e
specifica dei filosofi (in
examples\philosophers)
Attività
di
laboratorio su ASM multi-agenti. Esempi.
Soluzioni.
Caso
di studio di protocolli
crittografici: protocollo di Neeham-Sctraider,
modellazione della spia ed attacco di Lowe, protocollo di Neeham-Sctraider-Lowe,
modello
del
protocollo
con
la
spia
(esempi
di specifiche).
Model checking: Automi
di Kripke e logica CTL. Equivalenza tra formule CTL ed algoritmo di
model cheking.
Rappresentazione
di un automa di Kripke e di una formula CTL con ROBDD (Riduced
Ordered Binary Decision Diagrams)
Attività di
Laboratorio su model checking di specifiche ASM in AsmetaL.Primi
esempi. Esempi
del Bit Counter a Semaphore.
Caso di
studio di una centrale per lo smistamento di taxi su richiesta.
Avviso:
Per chiarimenti sull'uso di AsmetaS e per problemi
relativi alla simulazione di modelli ASM, potete contattare il Dott.
Paolo Arcaini alll'indirizzo
paolo.arcaini@unimi.it
Modalità
d'esame
Dal corrente anno accademico 2010-11, l'esame del corso consiste
in una prova scritta
(2 ore)
in una prova pratica
(2 ore) che solitamente va sostenuta nello stesso giorno della scritto,
oppure in appello successivo allo scritto. Su richiesta dello studente,
la prova pratica che può essere sostituita dalla presentazione
di un progetto la cui specifiche (più complesse rispetto a
quelle della prova pratica) verranno concordate con il docente dopo il
supertamento della prova scritta.
Partendo da semplici specifiche, durante la prova pratica lo studente
dovrà dimostrare di aver acquisito competenze sulla modellazione
ASM/AsmetaL, la simulazione di modelli con AsmetaS e la validazione
tratite AsmetaV, ed infine la verifica di
proprietà con AsmetaSMV.
L'eventuale progetto (in sostituzione della prova pratica)
dovrà prevedere anche la specifica (di
parte) dei requisiti in NuSMV e l'uso del model checker per la verifica
di opportune proprietà.
Nel definire i requisiti informali del progetto, occorre tenere
presente che la specifica finale deve soddisfare i seguenti vincoli:
deve essere una specifica ad agenti
deve prevedere l'uso di funzioni monitorate
deve prevedere un aspetto di non-determinismo (se possibile)
deve prevedere assiomi di stato
deve prevedere proprietà temporali significative
deve prevedere almeno un passo di raffinamento e la prova di
correttezza di questo