Summary
|
For Full-Text PDF, please login, if you are a member of IEICE, or go to Pay Per View on menu list, if you are a nonmember of IEICE. |
|
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(303.3KB)>>
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. | ||||||||||
| ||||||||||
