VERIFICA AUTOMATICA DEI SISTEMI: TEORIA E APPLICAZIONI

(CFU 9)

Prof. Angelo Montanari

Finalità

Il corso vuole presentare in modo sistematico metodi, formalismi e algoritmi proposti in ambito informatico per la specifica formale e la verifica automatica di sistemi reattivi complessi. Ampio spazio verrà dedicato alla teoria degli automi operanti su oggetti infiniti (parole e alberi) e alle logiche temporali (LTL, CTL, CTL*, mu-calculus). Particolare attenzione verrà riservata ai risultati relativi all'equivalenza espressiva tra classi di automi e sistemi logici. Verrà, inoltre, illustrato il possibile utilizzo della teoria logica dei giochi nella verifica formale. Dal punto di vista algoritmico, con riferimento ai modelli computazionali e ai formalismi di specifica presi in considerazione, verranno studiati in dettaglio gli algoritmi per la verifica della consistenza delle specifiche e della correttezza dei modelli. Un ruolo centrale verrà assegnato agli algoritmi di model checking, che consentono di validare il comportamento di un sistema hardware o software, descritto formalmente attraverso un modello matematico appropriato (ad esempio, un automa), rispetto alle proprietà attese del sistema, specificate mediante formule logiche (ad esempio, formule di CTL). In particolare, verranno presentate le soluzioni proposte per migliorare le prestazioni degli algoritmi di model checking (model checking simbolico, OBDD, partial order reduction). Verranno, inoltre, presi in esame alcuni esempi significativi di model checker. Nell'ultima parte del corso verranno introdotti alcuni temi di carattere più avanzato, quali, ad esempio, lo studio dei sistemi aperti e la verifica di sistemi a stati infiniti.

Programma 2012/13

Parte 1 - Introduzione ai sistemi reattivi.

Sistemi reattivi e real-time; sistemi di transizione equi; un semplice linguaggio di programmazione (SPL): sintassi e semantica, moduli; specifiche logiche e loro proprietà; l’uso della logica temporale per la specifica, la verifica e la validazione di programmi.

Parte 2 - Automi su oggetti infiniti

Automi su parole infinite: notazione, automi di Büchi, congruenze e complementazione, il calcolo sequenziale, determinismo e teorema di McNaughton; automi di Rabin e di Muller, elementi di teoria dei giochi; il teorema di McNaughton e Papert; omega-linguaggi star-free e logica temporale. Automi su alberi infiniti: notazione, automi su alberi, automi su alberi finiti, automi non deterministici di Büchi e di Rabin su alberi infiniti e loro relazioni, problema del vuoto e alberi regolari, complementazione e determinatezza dei giochi, teoria monadica degli alberi e risultati di decidibilità.

Parte 3 - Logiche modali e temporali

Introduzione, classificazione delle logiche temporali, le logiche temporali lineari, le logiche temporali ramificate, LTL, CTL, CTL* e mu-calculus, un ambiente per la modellazione della concorrenza: modelli astratti e concreti di concorrenza, concorrenza e logica temporale, espressività, decidibilità e complessità delle logiche temporali, algoritmi di satisfiability checking e di model checking.

Parte 4 - Verifica e validazione di sistemi reattivi

Algoritmi di satisfiability checking e di model checking per la verifica di programmi a stati finiti: soddisfacibilità e validità di una formula temporale, soddisfacibilità e validità di una formula temporale rispetto ad un programma a stati finiti, esempi, il problema della verifica di sistemi a stati infiniti (cenni).

Parte 5 – Model checking

Introduzione al model checking, model checking per LTL e CTL, massimi e minimi punti fissi di operatori monotoni, teorema di Tarski sulle approssimazioni, diagrammi di decisione binari ordinati (OBDD), model checking simbolico, automi alternanti e model checking, tecniche di partial order reduction, model checking per il mu-calculus (giochi di parità), esempi significativi di model checker.

Testi di riferimento:

A. Montanari, Linguaggi formali, automi e logiche, Note al Corso, 2011.

Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1992.

W. Thomas. Automata on Infinite Objects, in Handbook of Theoretical Computer Science - Vol. B (capitolo 4), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

W. Thomas. Languages, Automata, and Logic, in Handbook of Formal Languages, Vol. III, G. Rozenberg and A. Salomaa (eds.), Springer, pp. 389-455, 1997.

D. Perrin, J.-E. Pin, Infinite Words. Automata, Semigroups, and Games, Pure and Applied Mathematics Vol. 141, Elsevier, 2004.

E. A. Emerson. Temporal and Modal Logic, in Handbook of Theoretical Computer Science Vol. B (capitolo 16), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

Z. Manna, A. Pnueli. Temporal verification of Reactive Systems: Safety, Springer, 1995.

E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 2000.

Modalità d'esame

Homework e approfondimento

AUTOMATIC SYSTEM VERIFICATION: THEORY AND APPLICATIONS

(CFU 9)

Prof. Angelo Montanari

Objectives

The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal verification and automatic verification of complex reactive systems. A prominent role is assigned to the theory of automata operating on infinite objects (words and trees) and to temporal logics (LTL, CTL, CTL*, mu-calculus). A special attention is given to the expressive equivalence between classes of automata and logical systems. The possible role of the logical theory of games in formal verification is illustrated as well. From the algorithmic point of view, on the basis of the considered computational models and specification formalisms, the course studies in detail the main algorithms for specification consistency checking (satisfiability checking) and model checking. A special emphasis is given to model checking algorithms, that make it possible to validate the behaviour of hardware and software systems, modelled by means of a suitable mathematical model, e.g., an automaton, with respect to their formal requirements, specified by means of logical formulas, e.g., CTL formulas. In particular, the course described the main achievements in improving the performance of model checking algorithms(symbolic model checking, OBDD, partial order reduction). Moreover, a short description of meaningful examples of model checkers is given. In the last part of the course, some advanced topics are briefly introduced such as open systems and infinite state system verification.

Program 2012/13

PART 1 - Reactive Systems

Reactive and real-time systems, fair transition systems, transition diagram model and shared-variables text model, syntax and semantics of a simple programming language (SPL), modules, logical specifications and their properties, the use of temporal logic for the specification, verification, and validation of programs.

PART 2 - Automata on Infinite Objects

Automata on infinite words: notation, Büchi automata, congruence and complementation, the sequential calculus, determinism and McNaughton Theorem, Rabin and Muller automata; elements of logical game theory; McNaughton e Papert theorem; star-free omega-languages and temporal logic. Automata on infinite trees: notation, tree automata, automata on finite tree, Büchi and Rabin automata on infinite tree and their relationships, emptiness problem and regular trees, complementation and determinacy of games, monadic tree theory and decidability results, classification of Rabin recognizable sets.

PART 3 - Modal and Temporal Logic

Introduction, classification of temporal logics, linear temporal logics, branching temporal logics, LTL, CTL, CTL*, mu-calculus, concurrent computation: abstract and concrete computational models, concurrent computation and temporal logic, expressiveness, decidability, and complexity of temporal logic, satisfiability checking and model checking algorithms, other interesting modal and temporal logics in computer science.

PART 4 - Verification and Validation of Reactive Systems

Satisfiability checking and model checking algorithms for the verification of finite state programs: satisfiability and validity of temporal formulas, satisfiability and validity of temporal formulas with respect to a finite state program, examples, infinite state system verification (notes).

PART 5 – Model Checking

Introduction to model checking, LTL e CTL model checking, greatest and least fixpoints of monotonic operators, Tarski theorem on approximations, ordered binary decision diagrams (OBDD), symbolic model checking, alternating automata and model checking, partial order reduction techniques, model checking for the mu-calculus (parity games), meaningful examples of model checker.

References:

A. Montanari, Formal languages, automata, and logics, Lecture Notes, 2011.

Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1992.

W. Thomas. Automata on Infinite Objects, in Handbook of Theoretical Computer Science - Vol. B (Chapter 4), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

W. Thomas. Languages, Automata, and Logic, in Handbook of Formal Languages, Vol. III, G. Rozenberg and A. Salomaa (eds.), Springer, pp. 389-455, 1997.

D. Perrin, J.-E. Pin, Infinite Words. Automata, Semigroups, and Games, Pure and Applied Mathematics Vol. 141, Elsevier, 2004.

E. A. Emerson. Temporal and Modal Logic, in Handbook of Theoretical Computer Science Vol. B (Chapter 16), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

Z. Manna, A. Pnueli. Temporal Verification of Reactive Systems: Safety, Springer, 1995.

E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 2000.

Exam

Homework and elaboration