Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
8-2012
Abstract
Specification and verification of real-time systems are important research topics with crucial applications; however, the so-called state space explosion problem often prevents model checking to be used in practice for large systems. In this work, we present a self-contained toolkit to analyze real-time systems specified using event-recording automata (ERAs), which supports system modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that our tool outperforms the state-of-the-art timed model checker.
Keywords
Model Check, Proof Rule, Monolithic Approach, State Space Explosion Problem, UPPAAL Model
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 18th International Symposium Paris, France, 2012 August 27-31
First Page
272
Last Page
276
ISBN
9783642327582
Identifier
10.1007/978-3-642-32759-9_24
Publisher
Springer Link
City or Country
Paris, France
Citation
LIN, Shang-Wei; LIU, Yang; SUN, Jun; DONG, Jin Song; and ANDRÉ, Étienne.
Automatic compositional verification of timed systems. (2012). Proceedings of the 18th International Symposium Paris, France, 2012 August 27-31. 272-276.
Available at: https://ink.library.smu.edu.sg/sis_research/5016
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-32759-9_24