Please use this identifier to cite or link to this item:
Title: Build your own model checker in one month
Authors: Dong, J.S. 
Sun, J.
Liu, Y.
Issue Date: 2013
Citation: Dong, J.S.,Sun, J.,Liu, Y. (2013). Build your own model checker in one month. Proceedings - International Conference on Software Engineering : 1481-1483. ScholarBank@NUS Repository.
Abstract: Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. Applying model checking techniques to a new domain (which probably has its own dedicated modeling language) is, however, far from trivial. Translation-based approach works by translating domain specific languages into input languages of a model checker. Because the model checker is not designed for the domain (or equivalently, the language), translation-based approach is often ad hoc. Ideally, it is desirable to have an optimized model checker for each application domain. Implementing one with reasonable efficiency, however, requires years of dedicated efforts. In this tutorial, we will briefly survey a variety of model checking techniques. Then we will show how to develop a model checker for a language combining real-time and probabilistic features using the PAT (Process Analysis Toolkit) step-by-step, and show that it could take as short as a few weeks to develop your own model checker with reasonable efficiency. The PAT system is designed to facilitate development of customized model checkers. It has an extensible and modularized architecture to support new languages (and their operational semantics), new state reduction or abstraction techniques, new model checking algorithms, etc. Since its introduction 5 years ago, PAT has attracted more than 2500 registered users (from 500+ organisations in 60 countries) and has been applied to develop model checkers for 20 different languages. © 2013 IEEE.
Source Title: Proceedings - International Conference on Software Engineering
ISBN: 9781467330763
ISSN: 02705257
DOI: 10.1109/ICSE.2013.6606751
Appears in Collections:Staff Publications

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


checked on Dec 9, 2018

Page view(s)

checked on Dec 8, 2018

Google ScholarTM



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