Elementi di Software Dependability

Programma del Corso (9 CFU / 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: 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

Buchi 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.

*Gli argomenti indicati in corsivo non fanno parte del programma per gli studenti che intendono sostenere l'esame a 6 CFU.