Implementation of LMNtal Model Checkers: A Metaprogramming Approach

Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

研究成果: Article査読

1 被引用数 (Scopus)


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.

ジャーナルJournal of Object Technology
出版ステータスPublished - 2018 11月 1

ASJC Scopus subject areas

  • ソフトウェア


「Implementation of LMNtal Model Checkers: A Metaprogramming Approach」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。