INGLESE per la prima parte di 6 CFU che mutua B027561 (B059)
ITALAINO per la rimanente parte
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 Ingegneria dei Requisiti
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 software. 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 dei principi dell'Ingegneria dei requisiti
Conoscenza preliminare della disciplina delle software product lines
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, lezioni a distanza (emergenza COVID), esercitazioni personali in laboratorio
Altre Informazioni
Calendario degli Esami:
I appello 07/01/2021 10:00
II appello 21/01/2021 11:00
III appello 11/02/2021 11:00
IV appello 22/06/2021 11:00
V appello 08/07/2021 11:00
VI appello 22/07/2021 11:00
Date e orari indicativi: consultare preventivamente il docente
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
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.