Developing model checkers using PAT

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 langu...

Full description

Saved in:
Bibliographic Details
Main Authors: LIU, Yang, SUN, Jun, DONG, Jin Song
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2010
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/5034
https://ink.library.smu.edu.sg/context/sis_research/article/6037/viewcontent/Developing_Model_Checkers_Using_PAT.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-6037
record_format dspace
spelling sg-smu-ink.sis_research-60372020-03-12T08:35:05Z Developing model checkers using PAT LIU, Yang SUN, Jun DONG, Jin Song 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-09-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5034 info:doi/10.1007/978-3-642-15643-4_30 https://ink.library.smu.edu.sg/context/sis_research/article/6037/viewcontent/Developing_Model_Checkers_Using_PAT.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 Model Check Concurrent System Language Feature Symbolic Model Check Bound Model Check Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Model Check
Concurrent System
Language Feature
Symbolic Model Check
Bound Model Check
Programming Languages and Compilers
Software Engineering
spellingShingle Model Check
Concurrent System
Language Feature
Symbolic Model Check
Bound Model Check
Programming Languages and Compilers
Software Engineering
LIU, Yang
SUN, Jun
DONG, Jin Song
Developing model checkers using PAT
description 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.
format text
author LIU, Yang
SUN, Jun
DONG, Jin Song
author_facet LIU, Yang
SUN, Jun
DONG, Jin Song
author_sort LIU, Yang
title Developing model checkers using PAT
title_short Developing model checkers using PAT
title_full Developing model checkers using PAT
title_fullStr Developing model checkers using PAT
title_full_unstemmed Developing model checkers using PAT
title_sort developing model checkers using pat
publisher Institutional Knowledge at Singapore Management University
publishDate 2010
url https://ink.library.smu.edu.sg/sis_research/5034
https://ink.library.smu.edu.sg/context/sis_research/article/6037/viewcontent/Developing_Model_Checkers_Using_PAT.pdf
_version_ 1770575195639119872