Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/41107
Title: A CLP proof method for timed automata
Authors: Jaffar, J. 
Santosa, A. 
Voicu, R. 
Issue Date: 2004
Source: 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.

Page view(s)

71
checked on Dec 16, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.