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