Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
La Living Library di Scienze MM.FF.NN I corsi di Scienze MM.FF.NN
 
Le informazioni su questo Corso L'indice di tutte le lezioni Informazioni sulla Cattedra

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.

La Cattedra

Adriano Peron

Prof. 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”.

Curriculum completo

Anagrafica del corso

  • Scienze Matematiche Fisiche e Naturali, Università degli Studi di Napoli Federico II
  • Corsi di laurea: Informatica
  • Anno accademico: 2009/2010

Contatti

Indirizzo: Dipartimento di Scienze Fisiche, Complesso Universitario di Monte Sant'Angelo, Via Cintia, 21, Napoli (NA) - 80126

Telefono: 081.679280. Sito Web

  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion