Research in Logic Programming
Automatic Verification of Real-Time Systems using Logic Programming
We present a general constraint logic programming (CLP) based framework for specifying timed automata. In this framework a user specifies the grammar of the language accepted by the automata. The real-time constraints on transitions are captured in denotations of the grammar productions specified by the user. Thus, the grammar is specified as a Definite Clause Grammar (DCG), while the denotations are specified in constraint logic. The resulting specification is hence a constraint logic program (CLP), and is executable. Moreover, many interesting properties of the real-time system can be verified by posing appropriate queries to this CLP program. Our constraint-based methodology for specifying and verifying real-time systems is presented, and illustrated via examples. We also introduce a new type of automata called Constraint Automata that i s a generalization of timed automata.
Logic Prog. Page Research Page Lab Home Page