Verifying Real–Time Properties of tccp Programs

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.