Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
8-2012
Abstract
Model checking timed systems through digitization is relatively easy, compared to zone-based approaches. The applicability of digitization, however, is limited mainly for two reasons, i.e., it is only sound for closed timed systems; and clock ticks cause state space explosion. The former is mild as many practical systems are subject to digitization. It has been shown that BDD-based techniques can be used to tackle the latter to some extent. In this work, we significantly improve the existing approaches by keeping the ticks simple in the BDD encoding. Taking advantage of the ‘simple’ nature of clock ticks, we fine-tune the encoding of ticks and are able to verify systems with many ticks. Furthermore, we develop a BDD library which supports not only encoding/verifying of timed state machines (through digitization) but also composing timed components using a rich set of composition functions. The usefulness and scalability of the library are demonstrated by supporting two languages, i.e., closed timed automata and Stateful Timed CSP.
Keywords
Model Check, Linear Temporal Logic, Symbolic Model Check, Time Automaton, State Space Explosion
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
326
Last Page
340
ISBN
9783642327582
Identifier
10.1007/978-3-642-32759-9_28
Publisher
Springer Link
City or Country
Paris, France
Citation
NGUYEN, Truong Khanh; SUN, Jun; LIU, Yang; DONG, Jin Song; and LIU, Yan.
Improved BDD-based discrete analysis of timed systems. (2012). Proceedings of the 18th International Symposium Paris, France, 2012 August 27-31. 326-340.
Available at: https://ink.library.smu.edu.sg/sis_research/5017
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_28