Implementation of LMNtal Model Checkers: A Metaprogramming Approach

Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

研究成果: Article査読

抄録

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.

本文言語English
ジャーナルJournal of Object Technology
17
1
DOI
出版ステータスPublished - 2018 11 1

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

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

引用スタイル