The
Timed Concurrent
Constraint language (tccp) was defined by F. de Boer et al. as
an extension of the Concurrent
Constraint Paradigm (Saraswat, 1993) for specifying reactive and
embedded systems. In this paper, we describe the StructGenerator system
which, given the specification of a tccp program, constructs a symbolic
representation (a tccp Structure) modeling the behavior of such tccp
program. The resulting structure allows one to verify the program by
using a model-checking
algorithm. It is similar to a Kripke Structure but, due to the nature
of the ccp model, it differs from the classical approach in some
important points that will be described along the paper. The
StructGenerator system, implemented in C++, takes as input a file
containing the specification of a tccp program and generates the
associated tccp Structure. Along the paper, we cover the design and
implementation of StructGenerator. We also demonstrate its
functionality carrying out the execution of two practical examples.