Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/38953
Title: A reasoning method for timed CSP based on constraint solving
Authors: Dong, J.S. 
Hao, P.
Sun, J. 
Zhang, X.
Issue Date: 2006
Source: Dong, J.S.,Hao, P.,Sun, J.,Zhang, X. (2006). A reasoning method for timed CSP based on constraint solving. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4260 LNCS : 342-359. ScholarBank@NUS Repository.
Abstract: Timed CSP extends CSP by introducing a capability to quantify temporal aspects of sequencing and synchronization. It is a powerful language to model real time reactive systems. However, there is no verification tool support for proving critical properties over systems modelled using Timed CSP. In this work, we construct a reasoning method using Constraint Logic Programming (CLP) as an underlying reasoning mechanism for Timed CSP. We start with encoding the semantics of Timed CSP in CLP, which allows a systematic translation of Timed CSP to CLP. Powerful constraint solver like CLP(R) is then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, timewise refinement relationship, lower or upper bound of a time interval, etc. Counter-examples are generated when properties are not satisfied. Moreover, our method also handles useful extensions to Timed CSP. Finally, we demonstrate the effectiveness of our approach through case study of standard real time systems. © Springer-Verlag Berlin Heidelberg 2006.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/38953
ISBN: 3540474609
ISSN: 03029743
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

56
checked on Dec 8, 2017

Google ScholarTM

Check


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