Evolution of the LMNtal runtime to a parallel model checker

Masato Gocho, Taisuke Hori, Kazunori Ueda

    Research output: Contribution to journalArticle

    2 Citations (Scopus)

    Abstract

    Model checking is a verification technique based on the exhaustive search of erroneous behaviors of state transition systems, which is attracting growing interest. The LMNtal language allows us to represent state transition systems using hierarchical graph rewriting, and its runtime system, SLIM, has recently evolved into an explicit-state model checker. Hierarchical graphs are a powerful data structure that features a builtin symmetry reduction mechanism that plays a key role in state space search. However, model checking is still prone to state space explosion and has called for time- and space-efficient methods for state management. To address this problem and make our model checker more useful, we have extended the SLIM runtime further to a parallel model checker to run on shared-memory multiprocessors and developed various optimization techniques of state management. These two enhancements drastically improved the scale of problems the LMNtal model checker can handle as well as its performance.

    Original languageEnglish
    Pages (from-to)137-157
    Number of pages21
    JournalComputer Software
    Volume28
    Issue number4
    Publication statusPublished - 2011

    Fingerprint

    Model checking
    Hierarchical systems
    Explosions
    Data structures
    Data storage equipment

    ASJC Scopus subject areas

    • Software

    Cite this

    Evolution of the LMNtal runtime to a parallel model checker. / Gocho, Masato; Hori, Taisuke; Ueda, Kazunori.

    In: Computer Software, Vol. 28, No. 4, 2011, p. 137-157.

    Research output: Contribution to journalArticle

    Gocho, M, Hori, T & Ueda, K 2011, 'Evolution of the LMNtal runtime to a parallel model checker', Computer Software, vol. 28, no. 4, pp. 137-157.
    Gocho, Masato ; Hori, Taisuke ; Ueda, Kazunori. / Evolution of the LMNtal runtime to a parallel model checker. In: Computer Software. 2011 ; Vol. 28, No. 4. pp. 137-157.
    @article{bd1738d11fd244f68f6db5e3951da1c6,
    title = "Evolution of the LMNtal runtime to a parallel model checker",
    abstract = "Model checking is a verification technique based on the exhaustive search of erroneous behaviors of state transition systems, which is attracting growing interest. The LMNtal language allows us to represent state transition systems using hierarchical graph rewriting, and its runtime system, SLIM, has recently evolved into an explicit-state model checker. Hierarchical graphs are a powerful data structure that features a builtin symmetry reduction mechanism that plays a key role in state space search. However, model checking is still prone to state space explosion and has called for time- and space-efficient methods for state management. To address this problem and make our model checker more useful, we have extended the SLIM runtime further to a parallel model checker to run on shared-memory multiprocessors and developed various optimization techniques of state management. These two enhancements drastically improved the scale of problems the LMNtal model checker can handle as well as its performance.",
    author = "Masato Gocho and Taisuke Hori and Kazunori Ueda",
    year = "2011",
    language = "English",
    volume = "28",
    pages = "137--157",
    journal = "Computer Software",
    issn = "0289-6540",
    publisher = "Japan Society for Software Science and Technology",
    number = "4",

    }

    TY - JOUR

    T1 - Evolution of the LMNtal runtime to a parallel model checker

    AU - Gocho, Masato

    AU - Hori, Taisuke

    AU - Ueda, Kazunori

    PY - 2011

    Y1 - 2011

    N2 - Model checking is a verification technique based on the exhaustive search of erroneous behaviors of state transition systems, which is attracting growing interest. The LMNtal language allows us to represent state transition systems using hierarchical graph rewriting, and its runtime system, SLIM, has recently evolved into an explicit-state model checker. Hierarchical graphs are a powerful data structure that features a builtin symmetry reduction mechanism that plays a key role in state space search. However, model checking is still prone to state space explosion and has called for time- and space-efficient methods for state management. To address this problem and make our model checker more useful, we have extended the SLIM runtime further to a parallel model checker to run on shared-memory multiprocessors and developed various optimization techniques of state management. These two enhancements drastically improved the scale of problems the LMNtal model checker can handle as well as its performance.

    AB - Model checking is a verification technique based on the exhaustive search of erroneous behaviors of state transition systems, which is attracting growing interest. The LMNtal language allows us to represent state transition systems using hierarchical graph rewriting, and its runtime system, SLIM, has recently evolved into an explicit-state model checker. Hierarchical graphs are a powerful data structure that features a builtin symmetry reduction mechanism that plays a key role in state space search. However, model checking is still prone to state space explosion and has called for time- and space-efficient methods for state management. To address this problem and make our model checker more useful, we have extended the SLIM runtime further to a parallel model checker to run on shared-memory multiprocessors and developed various optimization techniques of state management. These two enhancements drastically improved the scale of problems the LMNtal model checker can handle as well as its performance.

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

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

    M3 - Article

    AN - SCOPUS:82755164958

    VL - 28

    SP - 137

    EP - 157

    JO - Computer Software

    JF - Computer Software

    SN - 0289-6540

    IS - 4

    ER -