Logic Prog. Page Research Page Lab Home Page
Author(s)Research in Logic Programming
Automatic Verification of Real-Time Systems using Logic Programming
Description
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.
Related Papers