PAT 3: An Extensible Architecture for Building Multi-Domain Model Checkers

Date Added: Aug 2011
Format: PDF

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 paper, the authors 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.