The
size and complexity of software systems are continuously increasing,
which makes them difficult and labor-intensive to develop, test and
evolve. Since concurrent systems are particularly hard to verify by
hand, achieving effective and automated verification tools for
concurrent software has become an important topic of research. Model checking is a popular
automated verification technology which allows us to determine the
properties of a software system and enables more thorough and less
costly testing. In this work, we improve the model-checking methodology
previously developed for the timed
concurrent constraint
programming language tccp so that more sophisticated, real-time
properties can be verified by the model-checking tools. The
contributions of the paper are twofold. On the one hand, we
define a timed extension of the tccp semantics which considers an
explicit, discrete notion of the passing of time. On the other hand,
we consistently define a real-time extension of the linear-time
temporal logic that is used to specify and analyze the software
properties in tccp. Both extensions fit into the tccp framework
perfectly in such a way that with minor modifications any tccp model
checker can be reused to analyze real-time properties. Finally, by
means of an example, we illustrate the improved ability to check
real-time properties.