Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2015

Abstract

Model checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. Firstly, given a system M1 M2, how do we automatically construct and refine (in the presence of spurious counterexamples) an assumption A2, which must be an abstraction of M2? Previous approaches suggest to incrementally learn and modify the assumption through multiple invocations of a model checker, which could be often time consuming. Secondly, how do we keep the state space small when checking M1 A2 |= ϕ if multiple refinements of A2 are necessary? Lastly, in the presence of multiple parallel components, how do we partition the components? In this work, we propose interpolationguided compositional verification. The idea is to tackle three challenges by using interpolations to generate and refine the abstraction of M2, to abstract M1 at the same time (so that the state space is reduced even if A2 is refined all the way to M2), and to find good partitions. Experimental results show that the proposed approach outperforms existing approaches consistently.

Keywords

model checking, automatic compositional verification, satisfiability, interpolation

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, Lincoln Nebraska, 2015 November 9-13

First Page

65

Last Page

74

ISBN

9781509000258

Identifier

10.1109/ASE.2015.33

Publisher

ACM

City or Country

Lincoln Nebraska

Additional URL

https://doi.org/10.1109/ASE.2015.33

Download

Share

COinS