Logiche temporali, formalismi di specifica, principi di prova e strumenti automatici di supporto alla verifica di sistemi software. Tecniche e algoritmi di base per lo sviluppo di "theorem prover" e di "model checker" e confronto di queste due diverse metodologie di verifica. Tecniche avanzate di model checking per la verifica di proprieta' sia quantitative che qualitative su sistemi software.
J.P, Katoen Concepts, Algorithms, and Tools for Model Checking
E.M. Clarke, O. Grumberg and D.A. Peled, Model Checking, MIT Press,
Cambridge, MA, USA, 1999.
J. Rutten, M. Kwiatkowska, G. Norman, D. Parker, Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Part II: Modelling and Verification of Probabilistic Systems. American Mathematical Society, USA, 2004.
C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, Model-Checking Algorithms for Continuous-Time Markov Chains, IEEE Transactions on Software Engineering, Vol. 29, Nr. 6, June 2003.
Obiettivi Formativi
Conoscenze:
Logiche temporali
Tecniche di verifica
Analisi formale di sistemi software
Logica Temporale Probabilistica
Logica Temporale Stocastica
Algoritmi di Model-Checking Probabilistica e Stocastica
Competenze acquisite
Utilizzazione di strumenti per l’analisi e verifica formale qualitativa e quantitativa di sistemi software
Capacità acquisite al termine del corso:
Capacita’ di impostare un processo di analisi e verifica formale di sistemi software.
Prerequisiti
Corsi raccomandati: Modelli di Sistemi Sequenziali e Concorrenti
Metodi Didattici
Numero di ore totali del corso: 150
Numero di ore per studio personale e altre attività formative di tipo individuale: 102
Numero di ore relative alle attività in aula: 48
Altre Informazioni
Orario di ricevimento
Martedi' 15,30- 16,30 previo appuntamento con il docente
Modalità di verifica apprendimento
Modalità:
Esame ed elaborato assegnato allo studente e svolto individualmente
Programma del corso
Lo scopo di questo corso e' quello di affrontare le relazioni tra i metodi di specifica, verifica e validazione in aree di ricerca diverse al fine di descrivere, sulla base di una teoria piu' generale, degli strumenti automatici di supporto allo sviluppo di sistemi affidabili, che siano applicabili anche in un contesto di produzione industriale. A questo proposito dobbiamo ricordare che la principale critica che viene mossa in contesto industriale nei confronti dei metodi formali e' che tali metodologie sono troppo costose e "time-consuming" per poter essere applicate efficacemente e su larga scala nell'industria. Quindi ai fini di un utilizzo efficiente dei metodi formali nell'industria e' indispensabile sviluppare strumenti automatici di supporto sufficientemente testati e con interfacce semplici, ed introdurre notazioni facilmente utilizzabili anche da tecnici non necessariamente esperti in metodi formali.
Nel corso verranno presentati formalismi di specifica, principi di prova e strumenti automatici di supporto alla specifica e verifica formale di proprieta' qualitative e quantitative di sistemi software.
In particolare saranno presentate le logiche temporali lineari e branching che sono riconosciute essere uno strumento efficace per la descrizione dei sistemi e delle loro proprieta’. Saranno poi presentati metodi di ' di verifica che si basano sull'analisi del modello comportamentale associati ad un particolare sistema. Piu' in particolare saranno presentate le tecniche e gli algoritmi di base per lo sviluppo di "model checkers", strumenti automatici per la prova di proprieta' dei sistemi che si basano sull'utilizzo del modello associato a tali sistemi.
Anche le estensioni probabilistiche e stocastiche di queste logiche verranno trattati, come per esempio PCTL e CSL. Queste logiche si basano su versioni etichettate delle Catene di Markov discrete e continue, rispettivamente. Saranno presentate gli algoritmi di model checking probabilistico/stocastico. Sara’ fornito anche una introduzione nell’uso di strumenti di model checking quantitativo.