Abstract
LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.
| Original language | English |
|---|---|
| Journal | Journal of Object Technology |
| Volume | 17 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 2018 Nov 1 |
Fingerprint
Keywords
- Graph rewriting
- Meta-interpreters
- Model checkers
- State- space search
ASJC Scopus subject areas
- Software
Cite this
Implementation of LMNtal Model Checkers : A Metaprogramming Approach. / Tsunekawa, Yutaro; Tomioka, Taichi; Ueda, Kazunori.
In: Journal of Object Technology, Vol. 17, No. 1, 01.11.2018.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Implementation of LMNtal Model Checkers
T2 - A Metaprogramming Approach
AU - Tsunekawa, Yutaro
AU - Tomioka, Taichi
AU - Ueda, Kazunori
PY - 2018/11/1
Y1 - 2018/11/1
N2 - LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.
AB - LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.
KW - Graph rewriting
KW - Meta-interpreters
KW - Model checkers
KW - State- space search
UR - http://www.scopus.com/inward/record.url?scp=85058782573&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85058782573&partnerID=8YFLogxK
U2 - 10.5381/jot.2018.17.1.a1
DO - 10.5381/jot.2018.17.1.a1
M3 - Article
AN - SCOPUS:85058782573
VL - 17
JO - Journal of Object Technology
JF - Journal of Object Technology
SN - 1660-1769
IS - 1
ER -