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)

Additional URL

https://doi.org/10.1109/TSE.2013.57

Share

COinS