Bounded model checking of compositional processes
Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2008
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5051 https://ink.library.smu.edu.sg/context/sis_research/article/6054/viewcontent/10.1.1.150.8078.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-6054 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-60542020-03-12T08:00:35Z Bounded model checking of compositional processes SUN, Jun LIU, Yang DONG, Jin Song SUN, Jing Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems. 2008-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5051 info:doi/10.1109/TASE.2008.12 https://ink.library.smu.edu.sg/context/sis_research/article/6054/viewcontent/10.1.1.150.8078.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 Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Software Engineering |
spellingShingle |
Software Engineering SUN, Jun LIU, Yang DONG, Jin Song SUN, Jing Bounded model checking of compositional processes |
description |
Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems. |
format |
text |
author |
SUN, Jun LIU, Yang DONG, Jin Song SUN, Jing |
author_facet |
SUN, Jun LIU, Yang DONG, Jin Song SUN, Jing |
author_sort |
SUN, Jun |
title |
Bounded model checking of compositional processes |
title_short |
Bounded model checking of compositional processes |
title_full |
Bounded model checking of compositional processes |
title_fullStr |
Bounded model checking of compositional processes |
title_full_unstemmed |
Bounded model checking of compositional processes |
title_sort |
bounded model checking of compositional processes |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2008 |
url |
https://ink.library.smu.edu.sg/sis_research/5051 https://ink.library.smu.edu.sg/context/sis_research/article/6054/viewcontent/10.1.1.150.8078.pdf |
_version_ |
1770575200244465664 |