Publication Type
Journal Article
Version
publishedVersion
Publication Date
1-2014
Abstract
Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, because constructing appropriate assumptions for AGR usually requires human creativity and experience. To automate compositional verification of timed systems, we propose a compositional verification framework using a learning algorithm for automatic construction of timed assumptions for AGR. We prove the correctness and termination of the proposed learning-based framework, and experimental results show that our method performs significantly better than traditional monolithic timed model checking.
Keywords
Automatic assume-guarantee reasoning, model checking, timed systems
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
IEEE Transactions on Software Engineering
Volume
40
Issue
2
First Page
137
Last Page
153
ISSN
0098-5589
Identifier
10.1109/TSE.2013.57
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Citation
LIN, Shang-Wei Lin; LIU, Yang; SUN, Jun; and SUN, Jun.
Learning assumptions for compositional verification of timed systems. (2014). IEEE Transactions on Software Engineering. 40, (2), 137-153.
Available at: https://ink.library.smu.edu.sg/sis_research/4982
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.1109/TSE.2013.57