The Community for Technology Leaders
RSS Icon
Subscribe
pp: 1
Shang-Wei Lin , National University of Singapore, Singapore
Étienne André , Université Paris, LIPN, CNRS, Paris
Yang Liu , Nanyang Technological University, Singapore
Jun Sun , Singapore University of Technology and Design, Singapore
Jin Song Dong , National University of Singapore, Singapore
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.
INDEX TERMS
Formal methods, Model checking
CITATION
Shang-Wei Lin, Étienne André, Yang Liu, Jun Sun, Jin Song Dong, "Learning Assumptions for Compositional Verification of Timed Systems", IEEE Transactions on Software Engineering, , no. 1, pp. 1, PrePrints PrePrints, doi:10.1109/TSE.2013.57
38 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool