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.
