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
La pervasività del software in una miriade di oggetti di cui ci serviamo ogni giorno per le più svariate attività è nota. Questa pervasività rende impellente la necessità che il software sia esente da guasti.
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 previsone dei guasti e di tolleranza ai guasti. Saranno studiati i costi dell'introduzione di queste tecniche in un contesto produttivo, e come il processo produttivo si debba relazionare a normative specifiche di alcuni settori di produzione industriale del software.
Capacità di impostare un processo di produzione del software mirato alla sua dependability
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
Realizzazione di un elaborato assegnato dal docente, e prova orale
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: ridondanza per diversità
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
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
Büchi automata - algoritmo di model checking per LTL
Labelled Transition Systems vs. Kripke Structures
Equivalenza di bisimulazione forte, Equivalenza osservazionale
Logica HML
Algebre di processi - CCS - Semantica operazionale
Logica ACTL
Modellazione di un sistema con Statecharts: i dialetti di Stateflow e Scade
Model Driven Development
I diagrammi di stato UML
Model checking su diagrammi a stati UML e su Statecharts
Strumenti di model checking: SMV, SPIN, UMC
Esercitazioni di modellazione e verifica formale
Model checking di codice C o Java
Analisi statica del codice: L’interpretazione astratta Lo strumento Polyspace
Le linee di prodotti software
Family Engineering vs. Product Engineering Modellazione di famiglie software
I feature diagrams
I principi dell’Ingegneria dei requisiti
Tracciamento dei requisiti
Strumenti di supporto alla gestione dei requisiti
Le Normative di sviluppo del software nei settori safety-critical: esempi di indicazioni date dalle normative.