Please use this identifier to cite or link to this item: https://doi.org/10.1145/2430536.2430537
Title: Modeling and verifying hierarchical real-time systems using stateful timed CSP
Authors: Sun, J.
Liu, Y.
Dong, J.S. 
Shi, L.
André, E. 
Keywords: Algorithms
Languages
Verification
Issue Date: 2013
Source: Sun, J.,Liu, Y.,Dong, J.S.,Shi, L.,André, E. (2013). Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Transactions on Software Engineering and Methodology 22 (1). ScholarBank@NUS Repository. https://doi.org/10.1145/2430536.2430537
Abstract: Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful Timed CSP models suffer from Zeno runs, that is, system runs that take infinitely many steps within finite time. Unlike Timed Automata, model checking with non-Zenoness in Stateful Timed CSP can be achieved based on the zone graphs. We extend the PAT model checker to support system modeling and verification using Stateful Timed CSP and show its usability/scalability via verification of real-world systems. © 2013 ACM.
Source Title: ACM Transactions on Software Engineering and Methodology
URI: http://scholarbank.nus.edu.sg/handle/10635/38952
ISSN: 1049331X
DOI: 10.1145/2430536.2430537
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

23
checked on Dec 12, 2017

Page view(s)

74
checked on Dec 8, 2017

Google ScholarTM

Check

Altmetric


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