PAT 3: An extensible architecture for building multi-domain model checkers
Model checking is emerging as an effective software verification method. Although it is desirable to have a dedicated model checker for each application domain, implementing one is rather challenging. In this work, we develop an extensible and integrated architecture in PAT3 (PAT version 3.*) to sup...
Saved in:
Main Authors: | , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2011
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5032 https://ink.library.smu.edu.sg/context/sis_research/article/6035/viewcontent/issre2011.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-6035 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-60352020-03-12T08:38:00Z PAT 3: An extensible architecture for building multi-domain model checkers LIU, Yang SUN, Jun DONG, Jin Song Model checking is emerging as an effective software verification method. Although it is desirable to have a dedicated model checker for each application domain, implementing one is rather challenging. In this work, we develop an extensible and integrated architecture in PAT3 (PAT version 3.*) to support the development of model checkers for wide range application domains. PAT3 adopts a layered design with an intermediate representation layer (IRL), which separates modeling languages from model checking algorithms so that the algorithms can be shared by different languages. IRL contains several common semantic models to support wide application domains, and builds both explicit model checking and symbolic model checking under one roof. PAT3 architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and even IRLs. Various model checkers have been developed under this new architecture in recent months. This paper discusses the structure and extensibility of this new architecture. 2011-11-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5032 info:doi/10.1109/ISSRE.2011.19 https://ink.library.smu.edu.sg/context/sis_research/article/6035/viewcontent/issre2011.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 LIU, Yang SUN, Jun DONG, Jin Song PAT 3: An extensible architecture for building multi-domain model checkers |
description |
Model checking is emerging as an effective software verification method. Although it is desirable to have a dedicated model checker for each application domain, implementing one is rather challenging. In this work, we develop an extensible and integrated architecture in PAT3 (PAT version 3.*) to support the development of model checkers for wide range application domains. PAT3 adopts a layered design with an intermediate representation layer (IRL), which separates modeling languages from model checking algorithms so that the algorithms can be shared by different languages. IRL contains several common semantic models to support wide application domains, and builds both explicit model checking and symbolic model checking under one roof. PAT3 architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and even IRLs. Various model checkers have been developed under this new architecture in recent months. This paper discusses the structure and extensibility of this new architecture. |
format |
text |
author |
LIU, Yang SUN, Jun DONG, Jin Song |
author_facet |
LIU, Yang SUN, Jun DONG, Jin Song |
author_sort |
LIU, Yang |
title |
PAT 3: An extensible architecture for building multi-domain model checkers |
title_short |
PAT 3: An extensible architecture for building multi-domain model checkers |
title_full |
PAT 3: An extensible architecture for building multi-domain model checkers |
title_fullStr |
PAT 3: An extensible architecture for building multi-domain model checkers |
title_full_unstemmed |
PAT 3: An extensible architecture for building multi-domain model checkers |
title_sort |
pat 3: an extensible architecture for building multi-domain model checkers |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2011 |
url |
https://ink.library.smu.edu.sg/sis_research/5032 https://ink.library.smu.edu.sg/context/sis_research/article/6035/viewcontent/issre2011.pdf |
_version_ |
1770575194488832000 |