Please use this identifier to cite or link to this item:
|Title:||A CLP proof method for timed automata||Authors:||Jaffar, J.
|Issue Date:||2004||Citation:||Jaffar, J.,Santosa, A.,Voicu, R. (2004). A CLP proof method for timed automata. Proceedings - Real-Time Systems Symposium : 175-186. ScholarBank@NUS Repository.||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. © 2004 IEEE.||Source Title:||Proceedings - Real-Time Systems Symposium||URI:||http://scholarbank.nus.edu.sg/handle/10635/41107||ISSN:||10528725|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Feb 19, 2020
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.