Elementi di Software Dependability
La pervasivita' del software in una miriade di oggetti di cui ci serviamo ogni giorno per le piu' svariate attivita' e' nota. Questa pervasivita' rende impellente la necessita' 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.
The current ubiquity of software, particularly inside objects that can have an impact on economy or on safety of people, prompts the need that software is bug-free.
This course wants to show a series of techniques that help avoiding the introduction of design errors in software production: mainly, formal development and verification techniques, but also fault forecasting and fault tolerance techniques.
The introduction of such techniques in a production context will be studied, and the relationships with guidelines of specific industrial production domains will be discussed.
Corso tenuto dal professor Alessandro Fantechi
Il materiale didattico si trova qui
-
Appunti scritti da Umberto Monile (PDF) file in formato ZIP
-
Appunti scannerizzati scritti da Mariano Di Claudio file in formato ZIP (circa 50 mega)
Interpretazione Astratta (PDF) file in formato ZIP
Verifica del Codice con interpretazione astratta (PDF - Seminario Daniele Grasso) file in formato ZIP
Software Safety (PDF) file in formato ZIP
Formal Methods in Practice (PDF - Alessio Ferrari) file in formato ZIP
Bounded Model Checking (PDF) file in formato ZIP
SAT-based Model Checking (PDF) file in formato ZIP
Model checking basato su Tableau (PDF - Stefano Boschi) file in formato ZIP
Relazione riguardante l'elaborato "Modellazione di un algoritmo di Railways Interlocking con Simulink Stateflow" di SImone Ercoli, Mariano Di Claudio e Dario Di Fina