(CoVer) Constraint-based Verification of Reactive systems

Data inizio
1 dicembre 2002
Durata (mesi) 
Responsabili (o referenti locali)
Giacobazzi Roberto
Parole chiave
verifica, vincoli, sistemi reattivi, interpretazione astratta, vincoli

Reactive systems are ubiquitous computer systems which maintain an ongoing interaction with an external environment, responding with appropriate actions to the external stimuli, and which often perform critical activities such as controlling industrial plants, managing financial transactions, scheduling time-critical operations, running e-commerce and web applications. With the increase of the dependency of our society from computer applications and reactive systems their correct behavior is becoming more and more critical, however their verification is particularly difficult. Practical examples of reactive systems in fact often consists of several sub-components that interact with an environment. Furthermore, their specification may require heterogeneous data and may depend on parameters whose values cannot be fixed a priori. Also, in many cases the set of possible states is infinite. Any of these aspects represents a big obstacle for the applicability of the state-of-the-art verification technology.

The scientific global goal of the project is to use the notion of `constraint', supported by abstract interpretation and type theory, as the unifying concept for the specification and automated verification of complex reactive systems.

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito dal Dipartimento

Partecipanti al progetto

Matteo Cristani
Professore associato
Roberto Giacobazzi
Professore ordinario
Isabella Mastroeni
Professore associato
Nicola Fausto Spoto
Professore associato