The
Timed Concurrent
Constraint programming language (tccp) introduces time aspects
into the Concurrent Constraint paradigm. This makes tccp especially
appropriate for analyzing timing properties of concurrent systems by
model checking. However, even if very compact state representations are
obtained thanks to the use of constraints in tccp, large state spaces
can still be generated, which may prevent model-checking tools from
verifying tccp programs completely. Model checking tccp programs
is a difficult task due to the subtleties of the underlying operational
semantics, which combines constraints, concurrency, non-determinism and
time. Currently, there is no practical model-checking tool that is
applicable to tccp. In this work, we introduce an abstract
methodology which is based on over- and under-approximating tccp models
and which mitigates the state explosion problem that is common to
traditional model-checking algorithms. We ascertain the
conditions for the correctness of the abstract technique and show that
this preliminary abstract semantics does not correctly simulate the
suspension behavior, which is a key feature of tccp. Then, we present a
refined abstract semantics which correctly models suspension. Finally,
we complete our methodology by approximating the temporal properties
that must be verified.