A constraint-based approach for specification and verification of real-time systems

We develop a general constraint logic programming (CLP) based framework for specification and verification of real-time systems. Our framework is based on the notion of timed automata that have traditionally been used for specifying real-time systems, In our framework, a user models the ordering of real-time events as the grammar of a language accepted by a timed automata, the real-time constraints on these events are then captured as denotations of the grammar productions specified by the user. The grammar can be specified as a Definite Clause Grammar (DCG), while the denotations can be specified in constraint logic. The resulting specification can hence be regarded as a constraint logic program (CLP), and is executable. Many interesting properties of the real-time system can be verified by posing appropriate queries to this CLP program. A major advantage of our approach is that it is constructive in nature, i.e., it can be used for computing the conditions under which a property will hold for a given real-time system. Our framework also suggests new types of formalisms that we call Constraint Automata and Timed Push-down Automata.