×

Executable structural operational semantics in Maude. (English) Zbl 1088.68095

Summary: This paper describes in detail how to bridge the gap between theory and practice when implementing in Maude structural operational semantics described in rewriting logic, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2. We validate this technique using it in several case studies: a functional language \(Fpl\) (evaluation and computation semantics), an imperative language \(WhileL\) (evaluation and computation semantics), Kahn’s functional language Mini-ML (evaluation or natural semantics), Milner’s CCS (with strong and weak transitions), and Full LOTOS (including ACT ONE data type specifications). In addition, on top of CCS we develop an implementation of the Hennessy-Milner modal logic for describing local capabilities of processes, and for LOTOS we build an entire tool where Full LOTOS specifications can be entered and executed (without user knowledge of the underlying implementation of the semantics). We also compare this method based on transitions as rewrites with another one based on transitions as judgements.

MSC:

68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science

Software:

Maude; ML; LOTOS; Coq; Eden
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Baalen, J. V.; Caldwell, J. L.; Mishra, S., Specifying and checking fault-tolerant agent-based protocols using Maude, (Rash, J.; Rouff, C.; Truszkowski, W.; Gordon, D.; Hinchey, M., First International Workshop, FAABS 2000, Greenbelt, MD, USA, April 2000. Revised Papers. First International Workshop, FAABS 2000, Greenbelt, MD, USA, April 2000. Revised Papers, Lecture Notes in Artificial Intelligence, vol. 1871 (2000), Springer: Springer Berlin), 180-193 · Zbl 0988.68743
[2] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, 14 (1987)
[3] Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J., Specification and proof in membership equational logic, Theoretical Computer Science, 236, 35-132 (2000) · Zbl 0938.68057
[4] Bradley, M.; Llana, L.; Martí-Oliet, N.; Robles, T.; Salvachua, J.; Verdejo, A., Transforming information in RDF to rewriting logic, (Peña, R.; Herranz, A.; Moreno, J. J., Segundas Jornadas sobre Programación y Lenguajes (PROLE 2002) (2002), El Escorial: El Escorial Madrid, Spain), 167-182
[6] Braga, C.; Hermann Haeusler, E.; Meseguer, J.; Mosses, P. D., Maude action tool: using reflection to map action semantics to rewriting logic, (Rus, T., Algebraic Methodology and Software Technology: 8th International Conference, AMAST 2000, Iowa City, IA, USA, May 2000, Proceedings. Algebraic Methodology and Software Technology: 8th International Conference, AMAST 2000, Iowa City, IA, USA, May 2000, Proceedings, Lecture Notes in Computer Science, vol. 1816 (2000), Springer: Springer Berlin), 407-421 · Zbl 0983.68519
[7] Braga, C.; Meseguer, J., Modular rewriting semantics of programming languages, (Algebraic Methodology and Software Technology: 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 2004, Proceedings (2004), Springer: Springer Berlin) · Zbl 1108.68401
[8] Breitinger, S.; Loogen, R.; Ortega-Mallén, Y.; Peña-Marí, R., Eden—The paradise of functional concurrent programming, (Bouge, L.; Fraigniaud, P.; Mignotte, A.; Robert, Y., Euro-Par ’96 Parallel Processing: Second International Euro-Par Conference, Lyon, France, August 26-29, 1996, Proceedings. Euro-Par ’96 Parallel Processing: Second International Euro-Par Conference, Lyon, France, August 26-29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1123 (1996), Springer: Springer Berlin), 710-713
[9] Bruni, R.; Meseguer, J., Generalized rewrite theories, (Baeten, J. C.M.; Lenstra, J. K.; Parrow, J.; Woeginger, G. J., Automata, Languages and Programming. 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003, Proceedings. Automata, Languages and Programming. 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2719 (2003), Springer-Verlag: Springer-Verlag Berlin), 252-266 · Zbl 1039.03020
[11] Calder, M.; Maharaj, S.; Shankland, C., A modal logic for Full LOTOS based on symbolic transition systems, The Computer Journal, 45, 1, 55-61 (2002) · Zbl 1008.68081
[14] Clavel, M., Reflection in Rewriting Logic: Metalogical Foundations and MetaprogramCSLI Publications (2000), CSLI Publications
[15] Clavel, M., The ITP tool, (Nepomuceno, A.; Quesada, J. F.; Salguero, J., Logic, Language and Information. Proceedings of the First Workshop on Logic and Language (2001), Kronos), 55-62
[17] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J., Maude: specification and programming in rewriting logic, Theoretical Computer Science, 285, 2, 187-243 (2002) · Zbl 1001.68059
[18] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., The Maude 2.0 system, (Nieuwenhuis, R., Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 2003, Proceedings. Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706 (2003), Springer: Springer Berlin), 76-87 · Zbl 1038.68559
[21] Cleaveland, R.; Sims, S. T., Generic tools for verifying concurrent systems, Science of Computer Programming, 42, 1, 39-47 (2002) · Zbl 0987.68780
[22] Degano, P.; Gadducci, F.; Priami, C., A causal semantics for CCS via rewriting logic, Theoretical Computer Science, 275, 1-2, 259-282 (2002) · Zbl 1026.68075
[23] Denker, G.; Millen, J., CAPSL integrated protocol environment, (Maughan, D.; Koob, G.; Saydjari, S., Proceedings DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25-27, 2000 (2000), IEEE Computer Society Press), 207-222, Available from:
[24] Despeyroux, T., Executable specification of static semantics, (Kahn, G.; MacQueen, D. B.; Plotkin, G. D., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, vol. 173 (1984), Springer: Springer Berlin), 215-233 · Zbl 0541.68003
[26] Durán, F.; Eker, S.; Lincoln, P.; Meseguer, J., Principles of Mobile Maude, (Kotz, D.; Mattern, F., Agent Systems, Mobile Agents, and Applications, Second International Symposium on Agent Systems and Applications and Fourth International Symposium on Mobile Agents, ASA/MA 2000, Zurich, Switzerland, September 13-15, 2000, Proceedings. Agent Systems, Mobile Agents, and Applications, Second International Symposium on Agent Systems and Applications and Fourth International Symposium on Mobile Agents, ASA/MA 2000, Zurich, Switzerland, September 13-15, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1882 (2000), Springer: Springer Berlin) · Zbl 0912.68095
[27] Eertink, H., Executing LOTOS specifications: the SMILE tool, (Bolognesi, T.; Lagemaat, J.; Vissers, C., LotoSphere: Software Development with LOTOS (1995), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht)
[28] Ehrig, H.; Mahr, B., (in: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. in: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science (1985), Springer: Springer Berlin) · Zbl 0557.68013
[29] Felty, A.; Gunter, E.; Hannan, J.; Miller, D.; Nadathur, G.; Scedrov, A., Lambda Prolog: An extended logic programming language, (Lusk, E.; Overbeek, R., 9th International Conference on Automated Deduction, Argonne, IL, USA, May 23-26, 1988, Proceedings. 9th International Conference on Automated Deduction, Argonne, IL, USA, May 23-26, 1988, Proceedings, Lecture Notes in Computer Science, vol. 310 (1988), Springer: Springer Berlin), 754-755
[30] Fernández, J. C.; Garavel, H.; Kerbrat, A.; Mounier, L.; Mateescu, R.; Sighireanu, M., CADP: a protocol validation and verification toolbox, (Alur, R.; Henzinger, T. A., Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, July 31-August 3, 1996, Proceedings. Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, July 31-August 3, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1102 (1996), Springer: Springer Berlin), 437-440
[31] Fernández, J. L.; Toval, A., Can intuition become rigorous? Foundations for UML model verification tools, (Titsworth, F. M., International Symposium on Software Reliability Engineering (2000), IEEE Press: IEEE Press San José, CA), 344-355
[32] Fernández, J. L.; Toval, A., Seamless formalizing the UML semantics through metamodels, (Siau, K.; Halpin, T., Unified Modeling Language: Systems Analysis, Design, and Development Issues (2001), Idea Group Publishing), 224-248
[33] (Gadducci, F.; Montanari, U., Proceedings Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002. Proceedings Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, Electronic Notes in Theoretical Computer Science, vol. 71 (2002), Elsevier: Elsevier Amsterdam), Available from: · Zbl 1001.68056
[34] Ghribi, B.; Logrippo, L., A validation environment for LOTOS, (Danthine, A.; Leduc, G.; Wolper, P., Protocol Specification, Testing and Verification XIII, Proceedings of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification, Liège, Belgium, May 25-28, 1993 (1993), North-Holland: North-Holland Amsterdam), 93-108
[35] Guillemot, R.; Haj-Hussein, M.; Logrippo, L., Executing large LOTOS specifications, (Aggarwal, S.; Sabnani, K., Protocol Specification, Testing, and Verification VIII, Proceedings of the IFIP TC6/WG6.1 Eighth International Symposium on Protocol Specification, Testing and Verification, Atlantic City, USA (1988), North-Holland: North-Holland Amsterdam), 399-410
[36] Hennessy, M., The Semantics of Programming Languages: An Elementary Introduction Using Structural Semantics (1990), John Wiley and Sons: John Wiley and Sons New York · Zbl 0723.68067
[37] Hennessy, M.; Lin, H., Symbolic bisimulations, Theoretical Computer Science, 138, 353-389 (1995) · Zbl 0874.68187
[38] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, Journal of the ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[39] Hidalgo-Herrero, M.; Ortega-Mallén, Y., An operational semantics for the parallel language Eden, Parallel Processing Letters, 12, 2, 211-228 (2002)
[40] Hirschkoff, D., A full formalisation of \(π\)-calculus theory in the calculus of constructions, (Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, Lecture Notes in Computer Science, vol. 1275 (1997), Springer: Springer Berlin), 153-169 · Zbl 0883.03012
[41] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[42] Honsell, F.; Miculan, M.; Scagnetto, I., \(π\)-Calculus in (co)inductive-type theory, Theoretical Computer Science, 253, 2, 239-285 (2001) · Zbl 0956.68095
[44] Ishikawa, H.; Meseguer, J.; Watanabe, T.; Futatsugi, K.; Nakashima, H., On the semantics of GAEA—An object-oriented specification of a concurrent reflective language in rewriting logic, (Proceedings IMSA’97 (1997), Information-Technology Promotion Agency: Information-Technology Promotion Agency Japan), 70-109
[46] Kahn, G., Natural semantics, (Brandenburg, F.-J.; Vidal-Naquet, G.; Wirsing, M., STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings. STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, Lecture Notes in Computer Science, vol. 247 (1987), Springer: Springer Berlin), 22-39 · Zbl 0657.68079
[47] (Kim, M.; Chin, B.; Kang, S.; Lee, D., Formal Techniques for Networked and Distributed Systems, FORTE 2001, IFIP TC6/WG6.1—21st International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea. Formal Techniques for Networked and Distributed Systems, FORTE 2001, IFIP TC6/WG6.1—21st International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea, IFIP Conference Proceedings, vol. 197 (2001), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht)
[48] (Kirchner, C.; Kirchner, H., Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, September 1-4, 1998. Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, September 1-4, 1998, Electronic Notes in Theoretical Computer Science, vol. 15 (1998), Elsevier: Elsevier Amsterdam), Available from: · Zbl 0903.00070
[49] Martí-Oliet, N.; Meseguer, J., Rewriting logic as a logical and semantic framework, (Gabbay, D. M.; Guenthner, F., Handbook of Philosophical Logic, vol. 9 (2002), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 1-87
[50] Martí-Oliet, N.; Meseguer, J., Rewriting logic: roadmap and bibliography, Theoretical Computer Science, 285, 2, 121-154 (2002) · Zbl 1027.68613
[51] Martí-Oliet, N.; Meseguer, J.; Verdejo, A., Towards a strategy language for Maude, (Martí-Oliet, N., Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004. Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, Electronic Notes in Theoretical Computer Science (2004), Elsevier: Elsevier Amsterdam), 391-414
[52] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96, 1, 73-155 (1992) · Zbl 0758.68043
[53] Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3-7, 1997, Selected Papers. Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3-7, 1997, Selected Papers, Lecture Notes in Computer Science, vol. 1376 (1998), Springer: Springer Berlin), 18-61 · Zbl 0903.08009
[54] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[55] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The Definition of Standard ML—Revised (1997), The MIT Press: The MIT Press Cambridge, MA
[56] Mosses, P. D., Foundations of modular SOS, (Kutylowski, M.; Pacholksi, L.; Wierzbicki, T., Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS’99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings. Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS’99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1672 (1999), Springer: Springer Berlin), 70-80, The full version appears as Technical Report RS-99-54, BRICS, Dept. of Computer Science, University of Aarhus · Zbl 0955.68075
[57] Nipkow, T., Winskel is (almost) right: towards a mechanized semantics textbook, Formal Aspects of Computing, 10, 2, 171-186 (1998) · Zbl 0910.68138
[58] Nipkow, T.; Paulson, L. C.; Wenzel, M., (in: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. in: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer: Springer Berlin) · Zbl 0994.68131
[59] Pettersson, M., RML—A new language and implementation for natural semantics, (Hermenegildo, M.; Penjam, J., Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP’94, Madrid, Spain, September 14-16, 1994, Proceedings. Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP’94, Madrid, Spain, September 14-16, 1994, Proceedings, Lecture Notes in Computer Science, vol. 844 (1994), Springer: Springer Berlin), 117-131
[60] Pettersson, M., (in: Compiling Natural Semantics. in: Compiling Natural Semantics, Lecture Notes in Computer Science, vol. 1549 (1999), Springer: Springer Berlin)
[61] Reynolds, J. C., Theories of Programming Languages (1998), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0972.68507
[62] Sprenger, C., A verified model checker for the modal \(μ\)-calculus in Coq, (Steffen, B., Ools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28-April 4, 1998, Proceedings. Ools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28-April 4, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1384 (1998), Springer: Springer Berlin), 167-183
[63] Stehr, M.-O., CINNI—A generic calculus of explicit substitutions and its application to \(λ-, ς\)- and \(π\)-calculi, (Futatsugi, K., Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000. Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, Electronic Notes in Theoretical Computer Science, vol. 36 (2000), Elsevier: Elsevier Amsterdam), 71-92, Available from:
[66] Stirling, C., Modal and temporal logics for processes, (Moller, F.; Birtwistle, G., Logics for Concurrency—Structure versus Automata, 8th Banff Higher Order Workshop, August 27-September 3, 1995, Proceedings. Logics for Concurrency—Structure versus Automata, 8th Banff Higher Order Workshop, August 27-September 3, 1995, Proceedings, Lecture Notes in Computer Science, vol. 1043 (1996), Springer: Springer Berlin), 149-237
[67] Terrasse, D., Encoding natural semantics in Coq, (Alagar, V. S., Lgebraic Methodology and Software Technology, 4th International Conference, AMAST ’95, Montreal, Canada, July 3-7, 1995, Proceedings. Lgebraic Methodology and Software Technology, 4th International Conference, AMAST ’95, Montreal, Canada, July 3-7, 1995, Proceedings, Lecture Notes in Computer Science, vol. 936 (1995), Springer: Springer Berlin), 230-244 · Zbl 1496.68119
[69] Toval, A.; Fernández, J. L., Formally modeling UML and its evolution: a holistic approach, (Smith, S. F.; Talcott, C. L., Proceedings IFIP Conference on Formal Methods for Open Object-Based Distributed Systems IV, FMOODS 2000, September 6-8, 2000, Stanford, CA, USA (2000), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 183-206 · Zbl 0968.68013
[70] Turner, K., Using Formal Description Techniques—An Introduction to Estelle, LOTOS and SDL (1992), John Wiley and Sons Ltd.: John Wiley and Sons Ltd. New York
[71] Verdejo, A., Building tools for LOTOS symbolic semantics in Maude, (Peled, D.; Vardi, M., Formal Techniques for Networked and Distributed Systems—FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, TX, USA, November 2002, Proceedings. Formal Techniques for Networked and Distributed Systems—FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, TX, USA, November 2002, Proceedings, Lecture Notes in Computer Science, vol. 2529 (2002), Springer: Springer Berlin), 292-307 · Zbl 1037.68516
[74] Verdejo, A.; Martí-Oliet, N., Implementing CCS in Maude, (Bolognesi, T.; Latella, D., Formal Methods For Distributed System Development, FORTE/PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 10-13, 2000, Pisa, Italy (2000), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 351-366
[77] Viry, P., Input/output for ELAN, (Meseguer, J., Proceedings First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, CA, September 3-6, 1996. Proceedings First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, CA, September 3-6, 1996, Electronic Notes in Theoretical Computer Science, vol. 4 (1996), Elsevier: Elsevier Amsterdam), 51-64, Available from: · Zbl 0912.68093
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.