Elementi di Software Dependability a.a. 2016-17

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, svolto dal Prof. Fantechi. Il secondo modulo, per gli ulteriori 3 CFU, verrà svolto dal Prof. Vicario.

Modulo 1 - A. Fantechi

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

Software mode checking. Concetti di astrazione. Analisi statica del codice: L'interpretazione astratta.


Modulo 2 - E. Vicario


Sequence of lectures, hosted in the course on Elements of Sw Dependability on the subject of stochastic models for quantitative evaluation in reliability engineering.

Lectures will combine theoretical stuff with practical modeling: to this end, attending students are recommended to have the Oris tool installed; this can be done simply by downloading and unzipping as documented at www.oris-tool.org.