la Correttezza del Software
_______________Primo Semestre 2016-17
Avvisi
4/1/2017
Completamento esami e verbalizzazione: giovedì 19/1/2017 ore 9:30 presso lo
studio del docente.
7/12/2016
Il giorno 13/12/2016 (martedì) alle 14 il Dott. Ing. Alberto Brescia Morra(Ericsson) terrà un seminario dal titolo:
"Continuous Integration and Test Automation practices in Ericsson''.
30/9/2016
Lista argomenti per seminari:
pdf
9/9/2016
La prima lezione del corso si terrà il giorno 23/9/2016
a partire dalle 9.15 presso l'aula F5.
Contestualmente, in base alle esigenze degli studenti e del docente, verrà stabilito
l'orario definitivo del corso.
Gli studenti interessati a seguire il corso sono pregati di contattare il
docente via email entro il 22/9/2015.
Modalità di esame
L'esame consiste nello svolgimento di un progetto/seminario di approfondimento su un argomento tra quelli introdotti al corso e in un colloquio orale.La parte principale del colloquio orale riguarda la discussione dei temi affrontati nel progetto/seminario.
Date di esame
Saranno inserite su Esse3 non appena saranno disponibili.
Programma
Il focus del corso è sulla verifica della correttezza e l'individuzione di errori nei programmi. Dopo una panoramica sugli strumenti e le tecniche utilizzate, verrà dato maggiore enfasi al testing (la pratica maggiormente diffusa a livello industriale) e al model-checking (una tecnica emergente completamente automatica capace di fornire una traccia di errore, e non solo l'individuazione di un bug).Il corso presenta contenuti di natura sia teorica che pratica, e prevede una sperimentazione delle metodologie studiate con l'ausilio di tool di verifica.
Il programma sarà dettagliato durante il corso e terrà conto anche delle preferenze manifestate dagli studenti alle lezioni.
Stampati delle lezioni
Saranno inserite di volta in volta (dopo le lezioni).- Concetti introduttivi
- Fondamenti di Model-checking
- Model-checking simbolico
- Bounded Model Checking
- Verifica con SPIN
- Linguaggio Promela
- Model-checking con automi pushdown
- Verifica con fixed-point calculus
- Sequenzializzazione di programmi concorrenti
- Tool CSeq
Seminari
- Analysis of Interacting BPEL Web Services (M. Villani)
- Automatic Generation of Test Cases (A. Sacco)
- Automi Temporizzati e UPPAAL (V. Ceci)
- Concolic Testing: jCUTE (G. Cantisani)
- mu-calculus Model Checking (R. D'Ambrosio)
- Program Repair as a Game (G. De Costanzo)
- Regular Model Checking (A. Zullo)
- A Tutorial on Runtime Verification (A. Ranieri)
- Separation Logic (L. Amitrano)
- Verifica di Programmi Periodici (A. Sheykina)
- Verifica di Sistemi Embedded (C. Iodice)
Testi di riferimento
- Gerard J. Holzmann
The SPIN Model Checker: Primer and Reference Manual
Addison Wesley, ISBN 0-321-22862-6. - Christel Baier and Joost-Pieter Katoen
Principles of model checking
The MIT Press, ISBN 978-0-262-02649-9 - Articoli scientifici
- Stampati delle lezioni