Insegnamento mutuato da: B024321 - SOFTWARE DEPENDABILITY Laurea Magistrale in INGEGNERIA INFORMATICA
Lingua Insegnamento
italiano
Contenuto del corso
Richiami di dependability
Software Reliability
Algoritmi distribuiti
Logica temporale e verifica formale Interpretazione astratta e Analisi statica Applicazioni delle tecniche di Verifica Formale Software product lines
Normative, contatti con le industrie
A. Fantechi - Informatica Industriale - Città Studi Edizioni
Dispense prodotte dal docente, disponibili sulla pagina web del docente
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. Il corso mira in particolare a fornire:
Conoscenza della disciplina della software reliability
Conoscenza di algoritmi distribuiti per tolleranza ai guasti
Conoscenza dei principali metodi formali
Conoscenza dei principi del model-based design
Conoscenza della teoria e delle tecniche della verifica formale di sistemi software
Conoscenza di tecniche di valutazione quantitativa di attributi di dependability basate su modelli stocastici *
Capacità di impostare un processo di produzione del software mirato alla sua dependability
Capacità di modellare correttamente il comportamento di un semplice sistema
Capacità di utilizzare strumenti di model-based design
Capacità di utilizzare strumenti per la verifica formale
Capacità di utilizzare strumenti di mediazione stocastica *
(*non incluse nel corso a 6 CFU)
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,
Prerequisiti
programmazione real-time, ingegneria del Software, dependability di sistemi hardware matematica discreta
informatica teorica
Metodi Didattici
Lezioni in aula, esercitazioni personali in laboratorio
Modalità di verifica apprendimento
La verifica finale consta di un elaborato assegnato dal docente, di norma ad un gruppo formato da due o tre studenti, e da una prova orale.
L’elaborato è mirato a dimostrare le capacità di:
- Saper modellare un sistema distribuito di media complessità secondo i canoni del model-based design
- Saper applicare strumenti di model-based design e di verifica formale sul modello oggetto dell’elaborato
- Saper definire un modello stocastico astraendo correttamente le caratteristiche salienti dal modello del sistema *
- Saper utilizzare uno strumento di valutazione quantitativa sul modello stocastico ottenuto *
(*non incluse nel corso a 6 CFU)
L’orale è mirato a valutare le conoscenze personali acquisite:
Conoscenza della disciplina della software reliability
Conoscenza di algoritmi distribuiti per tolleranza ai guasti
Conoscenza della teoria della modellazione formale e della verifica formale di sistemi software
Programma del corso
Il corso eroga 9 CFU.
C'è la possibilità di frequentare e dare l'esame per 6 CFU, seguendo solo il primo modulo.
Modulo 1 (6 CFU)
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
Algoritmi distribuiti - concetti di consistenza, validity e agreement
Memoria stabile
Checkpointing distribuito ed effetto domino
Two-phase commit protocol
Principio di incertezza
Paradosso dei generali bizantini
Byzantine Agreement: l'algoritmo ZA.
L'algoritmo di consistenza interattiva
Algoritmi di sincronizzazione di clock distribuiti
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
Labelled Transition Systems vs. Kripke Structures
Equivalenza di bisimulazione forte, Equivalenza osservazionale
Logica HML
Local model checking
Algebre di processi - CCS - Semantica operazionale - Equivalenza osservazionale
Logica ACTL
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 Scade
Strumenti di model checking: SMV, SPIN, UMC
Esercitazioni di modellazione e verifica formale
Modulo 2 (3 CFU)
Analisi statica del codice: L'interpretazione astratta.
Data-Flow Testing.
Software model checking.
Concetti di astrazione.
Counterexample-Guided Abstraction Refinement.
Ingegneria dei requisiti.