ITA | ENG
B010728 - ELEMENTI DI SOFTWARE DEPENDABILITY
Principali informazioni
Lingua Insegnamento
Contenuto del corso
Libri di testo consigliati
Obiettivi Formativi
Prerequisiti
Metodi Didattici
Altre Informazioni
Modalità di verifica apprendimento
Programma del corso
Anno Accademico 2013-14
Coorte 2013 - Laurea Magistrale in INGEGNERIA DELLE TELECOMUNICAZIONI
Anno di corso
Primo Anno - Secondo Semestre
Dipartimento di Afferenza
Ingegneria dell'Informazione
Tipo insegnamento
Attività formativa monodisciplinare
Settore Scientifico disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Crediti Formativi
6
Ore Didattica
48
Periodo didattico
03/03/2014 ⇒ 13/06/2014
Frequenza Obbligatoria
No
Tipo Valutazione
Voto Finale
Contenuto del corso
mostra
Programma del corso
mostra
Docenza
Mutuazione
Insegnamento mutuato da:
B010486 - ELEMENTI DI SOFTWARE DEPENDABILITY
Laurea Magistrale in INGEGNERIA INFORMATICA
B010486 - ELEMENTI DI 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
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
Libri di testo consigliati (Cerca nel catalogo della biblioteca)
A. Fantechi - Informatica Industriale - Città Studi Edizioni
Dispense prodotte dal docente, disponibili sulla pagina web del docente
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
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,
programmazione real-time,
ingegneria del Software,
dependability di sistemi hardware
matematica discreta
informatica teorica
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 ESAMI ELEMENTI DI SOFTWARE DEPENDABILITY
I Sessione:
- 10 gennaio 2013
- 31 gennaio 2013
- 21 febbraio 2013
II Sessione:
- 13 giugno 2013
- 4 luglio 2013
- 18 luglio 2013
III sessione:
- 5 Settembre 2013
Le date di esame fornite definiscono i momenti in cui il docente è disponibile per concordare l’elaborato. La prova orale verrà tenuta di norma dopo lo svolgimento dell’elaborato.
I Sessione:
- 10 gennaio 2013
- 31 gennaio 2013
- 21 febbraio 2013
II Sessione:
- 13 giugno 2013
- 4 luglio 2013
- 18 luglio 2013
III sessione:
- 5 Settembre 2013
Le date di esame fornite definiscono i momenti in cui il docente è disponibile per concordare l’elaborato. La prova orale verrà tenuta di norma dopo lo svolgimento dell’elaborato.
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.
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.