Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-15643-4_30
Title: Developing model checkers using PAT
Authors: Liu, Y. 
Sun, J. 
Dong, J.S. 
Issue Date: 2010
Source: Liu, Y.,Sun, J.,Dong, J.S. (2010). Developing model checkers using PAT. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6252 LNCS : 371-377. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-15643-4_30
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. © 2010 Springer-Verlag Berlin Heidelberg.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40014
ISBN: 3642156428
ISSN: 03029743
DOI: 10.1007/978-3-642-15643-4_30
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

16
checked on Dec 11, 2017

Page view(s)

51
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.