Interpolation guided compositional verification
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 automatica...
Saved in:
Main Authors: | , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2015
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4974 https://ink.library.smu.edu.sg/context/sis_research/article/5977/viewcontent/ASE.2015.33.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
Summary: | 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. |
---|