Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm

Kazuhiro OGATA  Kokichi FUTATSUGI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E90-A   No.8   pp.1690-1703
Publication Date: 2007/08/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e90-a.8.1690
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: Concurrent Systems
Keyword: 
Maude,  model checkers,  k-induction,  SAL,  the Suzuki-Kasami algorithm,  

Full Text: PDF>>
Buy this Article




Summary: 
SAL is a toolkit for analyzing transition systems, providing several different tools. Among the tools are a BDD-based symbolic model checker (SMC) and an SMT-based infinite bounded model checker (infBMC). The unique functionality provided by SAL is k-induction, which is supported by infBMC. Given appropriate lemmas, infBMC can prove automatically by k-induction that an infinite-state transition system satisfies invariant properties. Maude is a specification language and system based on membership equational logic and rewriting logic. Maude is equipped with an on-the-fly explicit state model checker. The unique functionality provided by the Maude model checker supports inductive data types. We make a comparison of SAL (especially SMC and infBMC) and the Maude model checker by conducting case studies in which the Suzuki-Kasami distributed mutual exclusion algorithm is analyzed. The purpose of the comparison is to clarify some of the two tools' functionalities, especially the unique ones, through the case studies.