Implementation of LMNtal Model Checkers: a Metaprogramming Approach
LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features an LTL model checker. There is some research on extensions of SLIM, and all of them achieve their functionalities by modifying SLIM. If a model checker is implemented in the modeling language itself, it should be very easy to develop prototypes of various model checkers without changing the implementation of the model checker. This approach is called metaprogramming which has been taken conventionally in Lisp and Prolog. In this paper, we define first-class rewriting rules to enable a metaprogramming in LMNtal. In addition to that, we design APIs to operate states of LMNtal programs. These features allow us to implement diverse variants of a model checker without changing SLIM. We implemented an LTL model checker and a CTL model checker in LMNtal. As a result, our framework is sufficient to develop a metainterpreter which treats program states flexibly.
| Paper (meta16-final5.pdf) | 239KiB |
Sun 30 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:30 - 10:00 | Model Checking and TransformationMETA at Matterhorn 3 Chair(s): Ralf Laemmel University of Koblenz-Landau, Germany | ||
08:30 30mTalk | Evolution of Metaprograms: XSLT as a Metaprogramming Language META Vadim Zaytsev Raincode, Belgium Media Attached File Attached | ||
09:00 30mTalk | Coloured Petri-Nets Framework for Simulating Method Invocations on Context-Oriented Software META Harumi Watanabe Tokai University, Ikuta Tanigawa Kyusyu University, Nobuhiko Ogura Tokyo City University, Midori Sugaya Shibaura Institute of Technology, Kenji Hisazumi Kyushu University, Akira Fukuda Kyushu University File Attached | ||
09:30 30mTalk | Implementation of LMNtal Model Checkers: a Metaprogramming Approach META Yutaro Tsunekawa Waseda University, Taichi Tomioka Waseda University, Kazunori Ueda Waseda University Media Attached File Attached | ||