TY - JOUR
T1 - The maude LTL model checker
AU - Eker, Steven
AU - Meseguer, José
AU - Sridharanarayanan, Ambarish
N1 - Funding Information:
The first two authors’ work has been partially supported by DARPA through Air Force Research Laboratory Contract F30602-97-C-0312, NSF grants CCR-9900326 and CCR-9900334, Office of Naval Research Contract N00012-99-C-0198, and DARPA through Air Force Research Laboratory Contract F30602-02-C-0130. The last two authors’ work is also supported in part by the ONR Grant N00014-02-1-0715. We specially thank Miguel Palomino for finding a gap in an earlier proof of the Theorem in Appendix B and suggesting the correct proof. We thank the members of the Maude team for their help in the design of this tool and in particular Narciso Martí-Oliet and Alberto Verdejo for carefully reading the manuscript and suggesting improvements. We also thank Leonardo De Moura, Amir Pnueli, and Tomás Uribe for very helpful discussions on temporal logic and model checking issues, Kousha Etessami for clarifying for us one of the ideas in his paper [8], Sam Owre for clarifying several aspects of the SAL language, and the anonymous referees for their constructive criticism on an earlier version of this paper.
PY - 2004/4
Y1 - 2004/4
N2 - The Maude LTL model checker supports on-the-fly explicit-state model checking of concurrent systems expressed as rewrite theories with performance comparable to that of current tools of that kind, such as SPIN. This greatly expands the range of applications amenable to model checking analysis. Besides traditional areas well supported by current tools, such as hardware and communication protocols, many new applications in areas such as rewriting logic models of cell biology, or next-generation reflective distributed systems can be easily specified and model checked with our tool.
AB - The Maude LTL model checker supports on-the-fly explicit-state model checking of concurrent systems expressed as rewrite theories with performance comparable to that of current tools of that kind, such as SPIN. This greatly expands the range of applications amenable to model checking analysis. Besides traditional areas well supported by current tools, such as hardware and communication protocols, many new applications in areas such as rewriting logic models of cell biology, or next-generation reflective distributed systems can be easily specified and model checked with our tool.
KW - Concurrent systems
KW - Maude
KW - Model checking
UR - http://www.scopus.com/inward/record.url?scp=19044397906&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=19044397906&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(05)82534-4
DO - 10.1016/S1571-0661(05)82534-4
M3 - Conference article
AN - SCOPUS:19044397906
SN - 1571-0661
VL - 71
SP - 162
EP - 187
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
T2 - WRLA 2002, Rewriting Logic and it's Applications
Y2 - 19 September 2002 through 21 September 2002
ER -