[4K2-OS-16b] [Organized Session] OS-16

[4K2-OS-16b-02] Implementation of LMNtal Model Checkers: a Metaprogramming Approach

〇Yutaro Tsunekawa¹, Kazunori Ueda¹ (1. Waseda University)

Keywords:Model Checking, Metaprogramming, Graph Rewriting System

LMNtalとはグラフ書き換えに基づくモデリング言語であり，そのモデル検査器SLIMは状態空間探索およびLTLモデル検査を備えている．
これまでSLIMに対して様々な拡張や変種が開発されてきたが，それらはすべてC言語で実装されたSLIMのソースコードを改変・修正することによって成されてきた．
本論文ではメタインタプリタを基礎にした容易に拡張可能なモデル検査器の実装のためのフレームワークを提案する．
フレームワークは(1)LMNtalにおける第一級の書き換え規則と(2)処理系SLIMに対するプログラム実行のためのAPIから成る．
これらの機能によってプログラマはLMNtalプログラムの状態遷移グラフを第一級のオブジェクトとしてLMNtalプログラム内で扱えるようになり，SLIMを変更することなく様々な変種を実装することが可能になる．
本研究ではLMNtalメタインタプリタを基礎にしてLTLモデル検査器，CTLモデル検査器，TCTLモデル検査器の実装および拡張を行った．