|
Published Articles >> Table of Contents >> Abstract
25th IEEE International Real-Time Systems Symposium (RTSS'04)
pp. 175-186
A CLP Proof Method for Timed Automata
Joxan Jaffar, National University of Singapore
Andrew Santosa, National University of Singapore
Razvan Voicu, National University of Singapore
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/REAL.2004.5
Send link to a friend
| Abstract |
|
Constraint Logic Programming (CLP) has been used to model programs and transition systems for the purpose of verification problems. In particular, it has been used to model Timed Safety Automata (TSA). In this paper, we start with a systematic translation of TSA into CLP. The main contribution is an expressive assertion language and a new CLP inference method for proving assertions. A distinction of the assertion language is that it can specify important properties beyond traditional safety properties. We highlight one important property: that a system of processes is symmetric. The new inference mechanism is based upon the well-known method of tabling in logic programming. It is distinguished by its ability to use assertions that are not yet proven, using a principle of coinduction. Apart from given assertions, the proof mechanism can also prove implicit assertions such as discovering a lower or upper bound of a variable. Finally, we demonstrate significant improvements over state-of-the-art systems using standard TSA benchmark examples.
|
 Additional Information
|
Citation:
Joxan Jaffar, Andrew Santosa, Razvan Voicu,
"A CLP Proof Method for Timed Automata,"
rtss,
pp. 175-186,
25th IEEE International Real-Time Systems Symposium (RTSS'04),
2004
|
|
