Verifica Automatica (Metodi D)

dott. Ivano Salvo
anno accademico 2004/05

Ultima modifica: 11 aprile 2005

Introduzione

Il corso ha l'obiettivo di presentare metodi e strumenti per la verifica automatica di sistemi concorrenti con particolare enfasi sui sistemi reattivi (e.g. sistemi operativi, protocolli, hardware digitale, sistemi embedded). Verranno descritti i formalismi di specifica basati su logiche temporali e gli algoritmi di verifica automatica (model checking) che sono alla base di molti tools accademici e commerciali per la validazione e verifica automatica di sistemi concorrenti.

Programma del corso

CTL, CTL*, LTL. Semantica. Strutture di Kriepke. Il problema del Model Checking esplicito. Model Checking Simbolico: teoremi di punto fisso classici (Knarster-Tarskij), caratterizzazione operatori CTL come punti fissi. OBDD. Witness e controesempi. Formalismi alternativi: mu-calcolo e automi di Buchi. Bounded Model Checking e SAT solver. Tecniche di riduzione del numero degli stati: astrazione. (Bi)similarità, simulazione, stuttering equivalence.

Materiale e testi di consultazione

Il testo seguito principalmente nel corso è il libro:

        Model Checking
Edmund M. Clarke, Jr, Orna Grumberg, and Doron A. Peled
MIT PRESS

Per la parte relativa al Bounded Model Checking, si vedano i seguenti lavori:

Orario

Modalità d'esame

L'esame consiste principalmente nello svolgimento di una tesina da parte degli studenti, che potrà avere sia carattere teorico (approfondimento di qualche argomento del corso, attraverso la lettura di articoli scientifici) o pratico (esempio di uso di un tool di verifica). Un altra parte dell'esame sarà costituita da un test semplice (ma da cui sono attesi risultati molto alti) volto a verificare la preparazione dello studente sugli argomenti trattati a lezione.

Diario delle Lezioni


[Fra parentesi i capitoli del libro di testo.]
[1] 15 marzo Introduzione al corso. Il problema della verifica dei programmi. Limiti e vantaggi di diversi approcci [1.1-1.3].

[2] 5 aprile Verifica di Sistemi concorrenti. Modellazione, specifica e verifica. Strutture di Kriepke. Descrizione di strutture di Kriepke con formule logiche [2].

[3] 7 aprile Specifica di Sistemi Concorrenti. La Logica Temporale CTL* e la sua semantica [3.1].

[4] 12 aprile Restrizioni di CTL*: LTL e CTL [3.2]. Il problema del Model Checking. Procedura di verifica per formule CTL [4.1].

[5] 14 aprile Procedura di verifica per formule LTL [4.2]. Fairness [3.3].

[6] 19 aprile Procedura di verifica per formule CTL* [4.3]. Strutture di Kriepke fair.

[7] 21 aprile Checking di proprietà di fairness [4.2].

[8] 26 aprile Esempi di esecuzioni degli algoritmi di Model Checking per CTL, LTL, e fair CTL [4].

[9] 28 aprile Punti fissi di operatori monotoni: teorema di Knarster-Tarskij. Teorema di Tarskij [NO]. Punti fissi nel caso di reticoli finiti [6.1].

[10,11] 3 maggio Caratterizzazione di proposizioni CTL come minimi e massimi punti fissi [6.2].
OBDD: definizione, calcolo delle principali funzioni [5.1]. Rappresentazione di strutture di Kriepke mediante OBDD [5.2].

[12] 5 maggio Model checking simbolico per CTL [6.2]. Vincoli di fairness [6.3]. Controesempi e Testimoni [6.4]

[13,14] 10 maggio mu-calcolo: sintassi, semantica, model checking e complessita'. Traduzione di CTL in mu-calcolo. [7]
Model checking simbolico per LTL [6.7 no dimostrazioni].

[15] 12 maggio Automi di Buchi [9.1, 9.2]. On-the-fly model checking [9.5]


[16,17] 17 maggio Problema dell'emptiness di linguaggi riconosciuti da automi di Buchi e controesempi all'emptiness. Algoritmo e sua correttezza e completezza [9.3].
Bounded Model Checking. Bounded Semantics per LTL.

[18] 19 maggio Trasformazione di un problema di Bounded Model Checking in un problema di soddisfacibilita' booleana. Procedura Davis-Putnam e sue ottimizzazioni.

[19,20] 24 maggio Partial Order Reduction: indipendenza, invisibilita', stuttering equivalence [10.1-2].

[21] 26 maggio Partial Order Reduction: ample set: caratterizzazione, calcolo. Euristiche [10.3, 10.5].

[22,23] 31 maggio Bisimulazioni e simulazioni tra strutture di Kriepke [11]
Invarianza di enunciati CTL* su strutture bisimili [11.1].

[24] 6 giugno Cenni ad astrazione e composizionalità [12,13: lettura senza dimostrazioni].