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

    Fingerprint

    Model checking
    Visualization
    Petri nets

    ASJC Scopus subject areas

    • Software

    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.

    LMNtal model checking using an integrated development environment. / Ayano, Takayuki; Hori, Taisuke; Iwasawa, Hiroki; Ogawa, Seiji; Ueda, Kazunori.

    In: Computer Software, Vol. 27, No. 4, 2010, p. 197-214.

    Research output: Contribution to journalArticle

    Ayano, T, Hori, T, Iwasawa, H, Ogawa, S & Ueda, K 2010, 'LMNtal model checking using an integrated development environment', Computer Software, vol. 27, no. 4, pp. 197-214.
    Ayano T, Hori T, Iwasawa H, Ogawa S, Ueda K. LMNtal model checking using an integrated development environment. Computer Software. 2010;27(4):197-214.
    Ayano, Takayuki ; Hori, Taisuke ; Iwasawa, Hiroki ; Ogawa, Seiji ; Ueda, Kazunori. / LMNtal model checking using an integrated development environment. In: Computer Software. 2010 ; Vol. 27, No. 4. pp. 197-214.
    @article{ee7768aaf2064e8a9eb5a660b8106815,
    title = "LMNtal model checking using an integrated development environment",
    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.",
    author = "Takayuki Ayano and Taisuke Hori and Hiroki Iwasawa and Seiji Ogawa and Kazunori Ueda",
    year = "2010",
    language = "English",
    volume = "27",
    pages = "197--214",
    journal = "Computer Software",
    issn = "0289-6540",
    publisher = "Japan Society for Software Science and Technology",
    number = "4",

    }

    TY - JOUR

    T1 - LMNtal model checking using an integrated development environment

    AU - Ayano, Takayuki

    AU - Hori, Taisuke

    AU - Iwasawa, Hiroki

    AU - Ogawa, Seiji

    AU - Ueda, Kazunori

    PY - 2010

    Y1 - 2010

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=78650850542&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=78650850542&partnerID=8YFLogxK

    M3 - Article

    AN - SCOPUS:78650850542

    VL - 27

    SP - 197

    EP - 214

    JO - Computer Software

    JF - Computer Software

    SN - 0289-6540

    IS - 4

    ER -