Scienze Matematiche Fisiche e Naturali » Tecniche di Specifica, Adriano Peron
Il Corso
Programma
Il corso si propone di fornire le nozioni di base per il problema della modellizzazione formale di sistemi Hardware e Software finalizzate alla verifica delle proprietà di correttezza. I formalismi considerati ricadono nella categoria dei formalismi Stato-Transizione (sia a stati finiti che infiniti).
In particolare si considerano gli Automi a stati finiti arricchiti anche con forme di rappresentazione esplicita del parallelismo e della comunicazione (sincrona e asincrona). Si considerano gli Automi di Buchi e di Muller per la descrizione di interazioni illimitate del sistema con il suo ambiente, per introdurre la nozione di fairness e la tecnica di verifica basata sulla teoria degli automi. Per la specifica delle proprietà si introduce la Logica Temporale Lineare (PLTL).
Tra i formalismi a stati infiniti, si considerano gli Automi a stati con pila, le Macchine a stati ricorsive e gli Automi temporizzati.
Il corso prevede esercitazioni su tool di specifica e verifica: SPIN (per gli automi a stati finiti), MOPED (per gli automi con pila) ed UPPAAL (per gli automi temporizzati).
Testi d'esame
- Dispense del corso a cura del docente.
- Tool SPIN.
- Articolo di riferimento: The Model Checker Spin, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.
- Tool MOPED
- Articolo di riferimento: J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs, In Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 324-336. Springer, 2001
- Tool UPPAAL.
- Articolo di riferimento: G. Behrmann, A. David and K.Larsen.
- A tutorial on UPPAAL.
Indice delle lezioni
1. Introduzione ai metodi formali di specifica
2. Semantica dei formalismi di specifica
3. Astrazione e Bisimulazione debole
4. FSM: Macchine a Stati Finiti
5. FSM: Non-determinismo e succintezza
7. FSM e Parallelismo – seconda parte
8. FSM e Parallelismo – terza parte
9. Promela
10. Specifica e verifica in SPIN
11. Proprietà di liveness in SPIN
12. Specifica di proprietà in Logica Temporale Lineare
13. Comportamenti infiniti: Automi di Büchi
14. Model checking di LTL basato su automi
15. Specifica di sistemi real time: Automi Temporizzati
16. Proprietà degli Automi Temporizzati
17. Problemi di decisione negli Automi Temporizzati
18. Il sistema di verifica UPPAAL
La Cattedra
Adriano Peron
Laureato in Scienze dell’Informazione presso l’Università di Udine nel 1988.
Dottore di Ricerca in Informatica presso l’Università di Pisa nel 1993 (V ciclo).
Ricercatore in Informatica (Settore scientifico – disciplinare K05B) dal 24 Giugno 1993 al 30 Ottobre 2001 presso la Facoltà di Lettere e Filosofia dell’Università di Udine.
Professore Associato in Informatica (Settore scientifico – disciplinare Inf/01) dal l Novembre 2001 al 31 gennaio 2005 presso la Facoltà di Scienze Matematiche Fisiche e Naturali dell’Università di Napoli “Federico II”.
E’ attualmente Professore Ordinario in Informatica (Settore scientifico – disciplinare Inf-01) presso la Facoltà di Scienze Matematiche Fisiche e Naturali dell’Università di Napoli “Federico II”. E’ attualmente Presidente del Consiglio dei Corsi di Studio in Informatica della Facoltà di Scienze Matematiche Fisiche e Naturali dell’Università di Napoli “Federico II”.
Anagrafica del corso
- Scienze Matematiche Fisiche e Naturali, Università degli Studi di Napoli Federico II
- Corsi di laurea: Informatica
- Anno accademico: 2009/2010
Contatti
