Metodi e Strumenti per la Verifica

Andrea Maggiolo Schettini    Tel. 0502212700

Scopo del corso è di esporre il problema della verifica di sistemi concorrenti e distribuiti usando diversi formalismi di specifica e tecniche di verifica.

Il corso introdurrà Reti di Petri, Statecharts, Automi temporizzati, affrontandone aspetti semantici e problemi di di verifica. Si presenteranno strumenti automatici che verranno utilizzati per sviluppare specifiche e prove per casi di esempio. Verranno anche proposti formalismi per la descrizione di sistemi biologici e metodi per la loro verifica.

The course will introduce formalisms fot the description of concurrent, distributed and real-time systems. In particular, Petri nets, Statecharts and Timed automata will be considered, and their semantical aspects and verification will be tackled. Automatic tools for specification and verification of properties will be described and used to develop specifications and verifications for sample cases. Also formalisms for the description of biological systems and their verification will be proposed.

Petri Nets, Statecharts, Timed Automata (36 ore); Strumenti software di sviluppo di specifica e di verifica (12 ore).

Riferimenti:
- per Reti di Petri:

• Reisig W., Petri Nets: An Introduction, Springer, Berlin, 1982.

- per Statecharts:

• Harel, D, A visual formalism for complex systems, Science of Computer programming 8 (1987) 271-274.

-per Automi Temporizzati:

• Alur R., Dill D.L., A Theory of Timed Automata, Theoretical Computer Science 126 (1994) 183-225.

-per P Systems:

• Paun, G., Membrane Computing: An Introduction, Springer, Berlin, 2002.