LMNtal model checking using an integrated development environment

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

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)197-214
Number of pages18
JournalComputer Software
Volume27
Issue number4
Publication statusPublished - 2010 Dec 1

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'LMNtal model checking using an integrated development environment'. Together they form a unique fingerprint.

  • Cite this

    Ayano, T., Hori, T., Iwasawa, H., Ogawa, S., & Ueda, K. (2010). LMNtal model checking using an integrated development environment. Computer Software, 27(4), 197-214.