LMNtal model checking using an integrated development environment

Takayuki Ayano*, Taisuke Hori, Hiroki Iwasawa, Seiji Ogawa, Kazunori Ueda

*この研究の対応する著者

研究成果: Article査読

1 被引用数 (Scopus)

抄録

LMNtal was designed and implemented as a unifying computational model based on hierarchical graph rewriting. In pursuit of its application to the fields of verification and search, the system has recently evolved into a model checker that employs LMNtal as a modeling language, and we have been accumulating experiences with modeling and verification. This paper describes LMNtalEditor, an integrated development environment (IDE) featuring both state space search and visualization of verification, and gives various examples of model description, verification and visualization. LMNtalEditor features the visualization and browsing of state space and counterexamples, the searching of states of interest, and so on. We have successfully run diverse examples taken from the fields including concurrency and AI search, and found that the IDE plays an essential role in understanding the models and counterexamples and thus greatly eases the task of verification. Furthermore, through the encoding of models in Promela, MSR and Coloured Petri Nets into LMNtal, we have extended the expressive power of LMNtal to the field of verification.

本文言語English
ページ(範囲)197-214
ページ数18
ジャーナルComputer Software
27
4
出版ステータスPublished - 2010 12月 1

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「LMNtal model checking using an integrated development environment」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル