The
language Timed Concurrent Constraint
(tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that
allows us to specify concurrent systems where timing is critical, for
example reactive systems.
Systems which may have an infinite number of states can be specified in
tccp. Model checking is a
technique which is able to verify finite-state systems with a huge
number of states in an automatic way. In the last years several studies
have investigated how to extend model checking techniques to systems
with an infinite number of states. In this paper we propose an approach
which exploits the computation model of tccp. Constraint based
computations allow us to define a methodology for applying a model
checking algorithm to (a class of) infinite-state systems. We extend
the classical algorithm of model checking for LTL to a specific logic
defined for the verification of tccp and to the tccp Structure which we
define in this work for modeling the program behavior. We define a
restriction on the time in order to get a finite model and then we
develop some illustrative examples. To the best of our knowledge this
is the first approach that defines a model checking methodology for
tccp.