Corso di Elementi di Software Dependabiity

1. Fantechi

Buona parte del corso tratta argomenti coperti dal libro:

A. Fantechi - Informatica Industriale - Città Studi Edizioni

(Errata-Corrige del libro "Informatica Industriale" )

In particolare, nella seguente trascrizione annotata del programma:

? gli argomenti marcati con L si trovano sul libro,

? quelli marcati con L + sono stati trattati in modo più approfondito, rispetto al libro

? quelli marcati con M sono argomenti trattati negli appunti raccolti da Umberto Monile, presenti in rete

? quelli marcati con * sono parti che non sono coperte da testi.

Sia per gli approfondimenti marcati con + che per gli argomenti marcati con *, non vi è ancora una raccolta sistematica di appunti, e quindi ci si può affidare a materiale che si trova in rete su questi argomenti, agli appunti di chi ha seguito, o alle slides presentate a lezione. Su alcuni argomenti, si può far riferimento al materiale linkato dalla pagina del vecchio corso di Informatica industriale II è disponibile. Gli argomenti marcati con *1, sono stati finora trattati in modo abbastanza superficiale, perciò è sufficiente il materiale introduttivo dipsonibile in rete.

==================

Richiami sui concetti di dependability di sistemi controllati da computer  L

Misure per la software dependability  L+

Software reliability: modelli di stima   L+

Tolleranza ai guasti software: ridondanza per diversità   L

Algoritmi distribuiti - concetti di consistenza, validity e agreement  L

Memoria stabile  L

Checkpointing distribuito ed effetto domino  L

Two-phase commit protocol  L

Principio di incertezza  L

Paradosso dei generali bizantini  L

Byzantine Agreement: l'algoritmo ZA.  L

L'algoritmo di consistenza interattiva  L

Algoritmi di sincronizzazione di clock distribuiti  L

Logica Modale  L

Logica Temporale  L

LTL - proprietà safety/liveness, proprietà di fairness , precedenza (until)  L

Proprietà di ricorrenza, minimo e massimo punto fisso  L

Logiche branching - CTL - interpretazione su Kripke Structures - CTL*  L

Algoritmo di Model Checking per CTL  L

Esplosione dello spazio degli stati  L

I Binary Decision Diagram (BDD) come tecnica di memorizzazione compatta dello spazio degli stati   L

Algoritmo di model checking basato su punto fisso   L

Buchi automata - algoritmo di model checking per LTL  M

Labelled Transition Systems vs. Kripke Structures  M

Equivalenza di bisimulazione forte, Equivalenza osservazionale  M

Logica HML  M

Algebre di processi - CCS - Semantica operazionale  M

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 L+

Lo strumento Polyspace  *

Le linee di prodotti software  *1

Family Engineering vs. Product Engineering  *1

Modellazione di famiglie software  *1

I feature diagrams  *1

I principi dell'Ingegneria dei requisiti  *1

Tracciamento dei requisiti  *1

Strumenti di supporto alla gestione dei requisiti  *1

Le Normative di sviluppo del software nei settori safety-critical: esempi di indicazioni date dalle normative  L