Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

9-2010

Abstract

During the last two decades, model checking has emerged as an effective system analysis technique complementary to simulation and testing. Many model checking algorithms and state space reduction techniques have been proposed. Although it is desirable to have dedicated model checkers for every language (or application domain), implementing one with effective reduction techniques is rather challenging. In this work, we present a generic and extensible framework PAT, which facilitates users to build customized model checkers. PAT provides a library of state-of-art model checking algorithms as well as support for customizing language syntax, semantics, state space reduction techniques, graphic user interfaces, and even domain specific abstraction techniques. Based on this design, model checkers for concurrent systems, real-time systems, probabilistic systems and Web Services are developed inside the PAT framework, which demonstrates the practicality and scalability of our approach.

Keywords

Model Check, Concurrent System, Language Feature, Symbolic Model Check, Bound Model Check

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 8th International Symposium, ATVA 2010, Singapore, September 21-24

First Page

371

Last Page

377

ISBN

9783642156427

Identifier

10.1007/978-3-642-15643-4_30

Publisher

Springer Link

City or Country

Singapore

Additional URL

https://doi.org/10.1007/978-3-642-15643-4_30

Download

Share

COinS