Richiami di dependability
Software Reliability
Metodi formali
Logica temporale e verifica formale, Model Checking
Interpretazione astratta e Analisi statica
Applicazioni delle tecniche di Verifica Formale
A. Fantechi - Informatica Industriale - Città Studi Edizioni
Dispense prodotte dal docente, disponibili su Moodle
Obiettivi Formativi
Il corso si propone di illustrare una serie di tecniche che consentono di ovviare per quanto possibile al problema dell'introduzione di errori di progetto nella produzione del software; quindi, principalmente, tecniche di verifica formale e di sviluppo formale del software, ma anche tecniche di previsione dei guasti e di tolleranza ai guasti software. Il corso mira in particolare a fornire:
Conoscenza della disciplina della software reliability
Conoscenza dei principali metodi formali
Conoscenza dei principi del model-based design
Conoscenza della teoria e delle tecniche della verifica formale di sistemi software
Prerequisiti
Costituisce prerequisito necessario per il corso
la conoscenza di tecniche di programmazione, in particolare in linguaggio C.
Risultano inoltre utili, per l'apprendimento di specifiche nozioni, conoscenze pregresse in:
sistemi operativi,
programmazione real-time, ingegneria del Software, dependability di sistemi hardware, matematica discreta,
informatica teorica
Metodi Didattici
Lezioni in aula, esercitazioni personali in laboratorio
Altre Informazioni
Calendario degli Esami:
da definire
Date e orari indicativi: consultare preventivamente il docente
Modalità di verifica apprendimento
La verifica finale consta di una prova orale
L’orale è mirato a valutare le conoscenze personali acquisite:
Conoscenza della disciplina della software reliability
Conoscenza della teoria della modellazione formale
Conoscenza dei principi e degli strumenti di verifica formale di sistemi software
Programma del corso
Richiami sui concetti di dependability di sistemi controllati da computer
Misure per la software dependability
Software reliability: modelli di stima
Tolleranza ai guasti software: Forward/Backward error recovery
Metodi Formali per lo sviluppo e la verifica del software
Metodi assiomatici, Z, B
Logica Modale
Logica Temporale
LTL - proprietà safety/liveness, proprietà di fairness , precedenza (until)
Proprietà di ricorrenza, minimo e massimo punto fisso
Logiche branching - CTL - interpretazione su Kripke Structures - CTL*
Algoritmo di Model Checking per CTL
Esplosione dello spazio degli stati
I Binary Decision Diagram (BDD) come tecnica di memorizzazione compatta dello spazio degli stati
Algoritmo di model checking basato su punto fisso
Buchi automata - algoritmo di model checking per LTL
Local model checking
Bounded Model Checking, con utilizzo di SAT solvers
Model Driven Development
I diagrammi di stato UML
Model checking su diagrammi a stati UML e su Statecharts
Modellazione di un sistema con Statecharts: i dialetti di Stateflow e UML
Strumenti di model checking: SMV, SPIN, UMC
Esercitazioni di modellazione e verifica formale
Analisi statica del codice: L'interpretazione astratta.
Software model checking.
Concetti di astrazione.
Counterexample-Guided Abstraction Refinement.