×

The Maude LTL model checker. (English) Zbl 1272.68243

Gadducci, Fabio (ed.) et al., WRLA 2002. Proceedings of the 4th international workshop on rewriting logic and its applications, Pisa, Italy, September 19–21, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 71, 162-187 (2004).
Summary: 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.
For the entire collection see [Zbl 1271.68038].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

SPIN; LTL2BA; Maude
PDFBibTeX XMLCite
Full Text: Link

References:

[1] Spin – Formal Verification. 2002.
[2] Clarke, E. M.; Grumberg, O.; Peled, D. A.: Model checking. (2001) · Zbl 0847.68063
[3] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.: Maude: specification and programming in rewriting logic. SRI international (January 1999) · Zbl 0917.68024
[4] Cohn, P. M.: Universal algebra. Harper & row (1965) · Zbl 0141.01002
[5] Dolev, D.; Klawe, M.; Rodeh, M.: An \(O(n \log n)\) unidirectional algorithm for extrema finding in a circle. Journal of algorithms 3, 245-260 (1982) · Zbl 0493.68074
[6] Eker S., Knapp M., Laderoute K. Lincoln, P. Talcott, C.L. Pathway logic: Executable models of biological networks. This volume.
[7] Eker, S.; Knapp, M.; Laderoute, K.; Lincoln, P.; Meseguer, J.; Sonmez, K.: Pathway logic: symbolic analysis of biological signaling. Proceedings of the Pacific symposium on biocomputing, 400-412 (January 2002)
[8] Etessami, K.; Holzmann, G. J.: Optimizing Büchi automata. Eleventh international conference on concurrency theory (CONCUR 2000), number 1877 in LNCS, 153-167 (2000) · Zbl 0999.68113
[9] Gastin, P.; Oddoux, D.: Fast LTL to Büchi automata translation. Thirteenth conference on computer aided verification (CAV ’01), number 2102 in LNCS, 53-65 (2001) · Zbl 0991.68044
[10] Gerth R. Concise Promela Reference. 1997.
[11] Gerth, R.; Peled, D.; Vardi, M.; Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. Protocol specification testing and verification, 3-18 (1995)
[12] Holzmann, G. J.; Peled, D.; Yannakakis, M.: On nested depth-first search. Proc. second SPIN workshop, August 1996, vol. 32 of DIMACS series in discrete mathematics and theoretical computer science 32, 81-89 (1997) · Zbl 0880.68084
[13] Yannakakis, G.; Holzmann, J.; Peled, D. M.: On nested depth first search. Design: an international journal 13, No. 3, 289-307 (1992)
[14] Manna Z. Pnueli A. The Temporal Logic of Reactive Systems. 1992 Springer-Verlag · Zbl 0753.68003
[15] Martí-Oliet, N.; Meseguer, J.: Rewriting logic as a logical and semantic framework. Technical report SRI-CSL-93-05, SRI international, computer science laboratory. To appear in handbook of philosophical logic (August 1993)
[16] Meseguer, J.; Talcott, C.: Semantic models for distributed object reflection. Proceedings of ECOOP’02, Malaga, Spain, June 2002, 1-36 (2002) · Zbl 1049.68815
[17] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, No. 1, 73-155 (1992) · Zbl 0758.68043
[18] Meseguer, J.: Membership algebra as a logical framework for equational specification. Proc. WADT’97, 18-61 (1998) · Zbl 0903.08009
[19] Meseguer, J.: Research directions in rewriting logic. Computational logic, NATO advanced study institute, marktoberdorf Germany, July 29 – August 6, 1997, 347-398 (1999) · Zbl 0940.68069
[20] Orava, F.; Parrow, J.: An algebraic verification of a mobile network. Formal aspects of computing 4, No. 6, 497-543 (1992) · Zbl 0782.68081
[21] Peterson, G. L.: Myths about the mutual exclusion problem. Information processing letters 12, No. 3, 115-116 (1981) · Zbl 0474.68031
[22] Shankar, N.: Symbolic analysis of transition systems. Abstract state machines: theory and applications (ASM 2000), number 1912 in lecture notes in computer science, 287-302 (mar 2000) · Zbl 0976.68518
[23] Somenzi, F. R.; Bloem, R.: Efficient Büchi automata from LTL formulae. Twelfth conference on computer aided verification (CAV ’00), number 1633 in LNCS, 247-263 (2000) · Zbl 0974.68086
[24] M.-O. Stehr and C. L. Talcott. Plan in Maude–specifying an active network programming language. This volume. · Zbl 1272.68044
[25] Viry, P.: Rewriting: an effective model of concurrency. PARLE’94, proc. Sixth int. Conf. on parallel architectures and languages Europe, Athens, Greece, July 1994, volume 817 of LNCS, 648-660 (1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.