Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2011

Abstract

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.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 22nd International Symposium on Software Reliability Engineering, Hiroshima, Japan, 2011 November 29 - December 11

First Page

1

Last Page

10

Identifier

10.1109/ISSRE.2011.19

Publisher

IEEE

City or Country

Hiroshima, Japan

Additional URL

https://doi.org/10.1109/ISSRE.2011.19

Download

Share

COinS