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 |
id |
sg-smu-ink.sis_research-5977 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59772020-03-12T07:30:49Z Interpolation guided compositional verification LIN, Shang-Wei SUN, Jun NGUYEN, Truong Khanh LIU, Yang DONG, Jin Song 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. 2015-11-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4974 info:doi/10.1109/ASE.2015.33 https://ink.library.smu.edu.sg/context/sis_research/article/5977/viewcontent/ASE.2015.33.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University model checking automatic compositional verification satisfiability interpolation Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
model checking automatic compositional verification satisfiability interpolation Software Engineering |
spellingShingle |
model checking automatic compositional verification satisfiability interpolation Software Engineering LIN, Shang-Wei SUN, Jun NGUYEN, Truong Khanh LIU, Yang DONG, Jin Song Interpolation guided compositional verification |
description |
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. |
format |
text |
author |
LIN, Shang-Wei SUN, Jun NGUYEN, Truong Khanh LIU, Yang DONG, Jin Song |
author_facet |
LIN, Shang-Wei SUN, Jun NGUYEN, Truong Khanh LIU, Yang DONG, Jin Song |
author_sort |
LIN, Shang-Wei |
title |
Interpolation guided compositional verification |
title_short |
Interpolation guided compositional verification |
title_full |
Interpolation guided compositional verification |
title_fullStr |
Interpolation guided compositional verification |
title_full_unstemmed |
Interpolation guided compositional verification |
title_sort |
interpolation guided compositional verification |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2015 |
url |
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 |
_version_ |
1770575163980513280 |