Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Sun 30 Oct 2016 09:30 - 10:00 at Matterhorn 3 - Model Checking and Transformation Chair(s): Ralf Lämmel

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 Oct
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:30 - 10:00: Meta 2016 - Model Checking and Transformation at Matterhorn 3
Chair(s): Ralf LämmelUniversity of Koblenz-Landau, Germany
meta201608:30 - 09:00
Vadim ZaytsevRaincode, Belgium
Media Attached File Attached
meta201609:00 - 09:30
Harumi WatanabeTokai University, Ikuta TanigawaKyusyu University, Nobuhiko OguraTokyo City University, Midori SugayaShibaura Institute of Technology, Kenji HisazumiKyushu University, Akira FukudaKyushu University
File Attached
meta201609:30 - 10:00
Yutaro TsunekawaWaseda University, Taichi TomiokaWaseda University, Kazunori UedaWaseda University
Media Attached File Attached