ACTIVITIES:

With the increase of dependency from computer applications, the correct behavior of software systems will become more and more critical for our society. In this scenario malfunctioning, inaccuracies or omissions will cause, in fact, major financial losses or even casualties. Widely known examples from the near past are the millennium bug and the Pentium bug.

Computer-aided verification is the research field devoted to the investigation of specialized algorithms and data structures for the automatic validation of hardware and protocols. Model checking and symbolic model checking are among the most popular techniques used for the verification of systems with a finite number of possible states. Symbolic model checking is based on the use of efficient data structures to represent compactly the state-space of finite-state systems during an exhaustive search for violations of a given functional properties.

Practical examples of reactive systems are often composed of a several subcomponents that interact with an environment. Furthermore, their specification may require data with heterogeneous types and possibly with parameters whose values is not fixed a priori. Any of these aspects represents a big obstacle for the applicability of standard verification technology.

The correctness of a system can be explored by scanning all possible executions using symbolic representations of the state space. However this method will not scale up with the size and complexity of the system. Furthermore, though model checking can find potential bugs, it cannot provide proofs of correctness.

We propose to use constraints as a mathematical concept to attack verification problems for systems consisting of several components defined over heterogeneous and possibly unbounded data, and presenting parameters in their specification.

A constraint can be viewed as a formula representing a relation defined over a fixed domain. A constraint solver is a procedure implementing operations like variable elimination, satisfiability test, entailment of solutions defined over the considered domain. Constraint languages can be naturally used to specify in a compact way the data relation of a reactive system.

The passage from boolean logic to constraint solving gives us a natural way to investigate verification problems for reactive systems with a potentially infinite state space.

Constraints can also be important in the case of finite-state systems, where they allow to control the state-explosion problem that, in many cases, makes the use of verification tools computationally impossible since the number of states can grow exponentially with the number of the components of the system.