×

zbMATH — the first resource for mathematics

Two case studies of semantics execution in Maude: CCS and LOTOS. (English) Zbl 1086.68552
Summary: We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two substantial case studies. In the first one, we represent both the semantics of Milner’s CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics is already known, it cannot be directly executed in the default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by controlling the rewriting process by means of reflection. This executable specification plus the reflective control of rewriting can be used to analyze CCS processes. The same techniques are also used to implement a symbolic semantics for LOTOS in our second case study. The good properties of Maude as a metalanguage allow us to implement a whole formal tool where LOTOS specifications without restrictions in their data types (given as ACT ONE specifications) can be executed. In summary, we present Maude as an executable semantic framework by providing easy-tool-building techniques for a language given its operational semantics.

MSC:
68Q42 Grammars and rewriting systems
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.)
03B70 Logic in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] S. Berghofer, ”Proofs, programs and executable specifications in higher order logic,” PhD thesis, Institut für Informatik, Technische Universität München, 2003. · Zbl 1023.68021
[2] S. Berghofer and T. Nipkow, ”Executing higher order logic,” in P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (Eds.), Types for Proofs and Programs: International Workshop, TYPES 2000, Durham, UK, Selected Papers, Vol. 2277 of Lecture Notes in Computer Science, Springer-Verlag, 2002. · Zbl 1054.68133
[3] P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. ”An overview of ELAN,” in Kirchner and Kirchner [38], pp. 329–344. · Zbl 0917.68022
[4] R. Bruni, ”Tile logic for synchronized rewriting of concurrent systems,” PhD thesis, Dipartimento di Informatica, Università di Pisa, 1999.
[5] R. Bruni, J. Meseguer, and U. Montanari, ”Internal strategies in a rewriting implementation of tile systems,” in Kirchner and Kirchner [38]. · Zbl 0917.68104
[6] M. Calder and C. Shankland, ”A symbolic semantics and bisimulation for Full LOTOS,” in M. Kim, B. Chin, S. Kang, and D. Lee (Eds.), Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems, Kluwer Academic Publishers, 2001, pp. 184–200.
[7] W. Chen and D.S. Warren, ”Tabled evaluation with delaying for general logic programs,” Journal of the ACM, Vol. 43, No. 1, pp. 20–74, 1996. · Zbl 0882.68050
[8] M. Clavel, Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Application, CSLI Publications, 2000. · Zbl 1003.03032
[9] M. Clavel, ”The ITP tool,” in A. Nepomuceno, J.F. Quesada, and J. Salguero, (Eds.), Logic, Language and Information. Proceedings of the First Workshop on Logic and Language, Kronos, 2001, pp. 55-62.
[10] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada, ”Maude as a metalanguage,” in Kirchner and Kirchner [38]. · Zbl 0917.68106
[11] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada, Maude: Specification and Programming in Rewriting Logic, Computer Science Laboratory, SRI International, 1999. http://maude.cs.uiuc.edu/maude1/manual. · Zbl 1001.68059
[12] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada, A Maude Tutorial, Computer Science Laboratory, SRI International, 2000. http://maude.cs.uiuc.edu/papers.
[13] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada, ”Using Maude,” in T. Maibaum (Ed.), Proc. Third Int. Conf. Fundamental Approaches to Software Engineering, FASE 2000, Berlin, Germany, March/April 2000, Vol. 1783 of Lecture Notes in Computer Science, Springer, 2000, pp. 371-374. · Zbl 0917.68024
[14] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada, ”Maude: Specification and programming in rewriting logic,” Theoretical Computer Science, Vol.ol. 285, No. 2, pp. 187–243, 2002. · Zbl 1001.68059
[15] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J.F. Quesada, ”Towards Maude 2.0,” in K. Futatsugi (Ed.), Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, vol. 36 of Electronic Notes in Theoretical Computer Science, Elsevier, 2000, pp. 297–318.
[16] M. Clavel, F. Durán, S. Eker, J. Meseguer, and M.-O. Stehr, ”Maude as a formal meta-tool,” in J. Wing, J. Woodcock, and J. Davies (Eds.), FM’99–Formal Methods, Proc. World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Vol. II, vol. 1709 of Lecture Notes in Computer Science, Springer, 1999, pp. 1684–1703.
[17] M. Clavel and J. Meseguer, ”Axiomatizing reflective logics and languages,” in G. Kiczales (Ed.), Proceedings of Reflection’96, 1996, pp. 263–288.
[18] M. Clavel and J. Meseguer, ”Reflection in conditional rewriting logic,” Theoretical Computer Science, Vol. 285, No. 2, pp. 245–288, 2002. · Zbl 1001.68060
[19] R. Cleaveland, E. Madelaine, and S.T. Sims, ”A front-end generator for verification tools,” in Proc. of the Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’95), vol. 1019 of Lecture Notes in Computer Science, Springer, 1995, pp. 153–173.
[20] R. Cleaveland and S.T. Sims, ”Generic tools for verifying concurrent systems,” Science of Computer Programming, Vol. 42, No. 1, pp. 39-47, 2002. · Zbl 0987.68780
[21] B. Cui, Y. Dong, X. Du, K.N. Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, A. Roy-choudhury, S.A. Smolka, and D.S. Warren, ”Logic programming and model checking,” in C. Palamidessi, H. Glaser, and K. Meinke (Eds.), Principles of Declarative Programming: 10th International Symposium, PLILP’98. Held Jointly with the 6th International Conference, ALP’98, Pisa, Italy, Proceedings, vol. 1490 of Lecture Notes for Computer Science, Springer, 1998, pp. 1–20.
[22] T. Despeyroux, ”Executable specification of static semantics,” in G. Kahn, D.B. MacQueen, and G.D. Plotkin (Eds.), Semantics of Data Types, vol. 173 of Lecture Notes in Computer Science, Springer, 1984. pp. 215-233. · Zbl 0541.68003
[23] T. Despeyroux, ”TYPOL: A formalism to implement natural semantics,” Research Report 94, INRIA, 1988.
[24] F. Durán, ”A reflective module algebra with applications to the Maude language,” PhD thesis, Universidad de Málaga, 1999.
[25] H. Eertink, ”Executing LOTOS specifications: The SMILE tool,” in T. Bolognesi, J. Lagemaat, and C. Vissers (Eds.), LotoSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995.
[26] H. Ehrig and B. Mahr, ”Fundamentals of algebraic specification 1: Equations and Initial Semantics,” EATCS Monographs on Theoretical Computer Science, Springer, 1985. · Zbl 0557.68013
[27] J.C. Fernández, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu, ”CADP: A protocol validation and verification toolbox,” in R. Alur and T. A. Henzinger (Eds.), Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, Proceedings, vol. 1102 of Lecture Notes in Computer Science, Springer, 1996, pp. 437–440.
[28] B. Ghribi and L. Logrippo, ”A validation environment for LOTOS,” in A. Danthine, G. Leduc, and P. Wolper (Eds.), 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, North-Holland, 1993, pp. 93–108.
[29] M. Gordon and T. Melham, ”Introduction to HOL: A theorem proving environment for higher order logic,” Cambridge University Press, 1993. · Zbl 0779.68007
[30] R. Guillemot, M. Haj-Bussein, and L. Logrippo, ”Executing large LOTOS specifications,” in S. Aggarwal and K. Sabnani (Eds.), 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, North-Holland, 1988, pp. 399–410.
[31] M. Hennessy and H. Lin, ”Symbolic bisimulations,” Theoretical Computer Science, Vol. 138, pp. 353–389, 1995. · Zbl 0874.68187
[32] M. Hennessy and R. Milner, ”Algebraic laws for nondeterminism and concurrency,” Journal of the ACM, Vol. 32, No. 1, pp. 137–161, 1985. · Zbl 0629.68021
[33] D. Hirschkoff, ”A full formalisation of {\(\pi\)}-calculus theory in the calculus of constructions,” in Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, Proceedings, vol. 1275 of Lecture Notes in Computer Science, Springer, 1997, pp. 153–169. · Zbl 0883.03012
[34] C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985. · Zbl 0637.68007
[35] F. Honsell, M. Miculan, and I. Scagnetto, ”{\(\pi\)}-calculus in (co)inductive-type theory,” Theoretical Computer Science, Vol. 253, No. 2, pp. 239–285, 2001. · Zbl 0956.68095
[36] G. Huet, G. Kahn, and C. Paulin-Mohring, ”The Coq proof assistant: A tutorial: version 7.2,” Technical Report 256, INRIA, 2002.
[37] ISO/IEC, ”LOTOS-A formal description technique based on the temporal ordering of observational behaviour,” International Standard 8807, International Organization for standardization–Information Processing Systems–Open Systems Interconnection, Geneva, 1989.
[38] C. Kirchner and H. Kirchner (Eds.), Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, vol. 15 of Electronic Notes in Theoretical Computer Science, Elsevier, 1998.
[39] Z. Luo and R. Pollack, ”The LEGO proof development system: A user’s manual,” Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992.
[40] N. Martí-Oliet and J. Meseguer, ”Rewriting logic as a logical and semantic framework,” in D. M. Gabbay and F. Guenthner (Eds.), Handbook of Philosophical Logic, Second Edition, vol. 9, Kluwer Academic Publishers, 2002, pp. 1–87.
[41] N. Martí-Oliet and J. Meseguer, ”Rewriting logic: Roadmap and bibliography,” Theoretical Computer Science, Vol. 285, No. 2, pp. 121–154, 2002. · Zbl 1027.68613
[42] T.F. Melham, ”A mechanized theory of the {\(\pi\)}-calculus in HOL,” Nordic Journal of Computing, Vol. 1, No. 1, pp. 50–76, 1994.
[43] J. Meseguer, ”Conditional rewriting logic as a unified model of concurrency,” Theoretical Computer Science, Vol. 96, No. 1, pp. 73–155, 1992. · Zbl 0758.68043
[44] J. Meseguer, ”Research directions in rewriting logic,” in U. Berger and H. Schwichtenberg (Eds.), Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, NATO ASI Series F: Computer and Systems Sciences 165, Springer, 1998, pp. 347–398. · Zbl 0940.68069
[45] J. Meseguer, K. Futatsugi, and T. Winkler, ”Using rewriting logic to specify, program, integrate, and reuse open concurrent systems of cooperating agents,” in Proceedings of the 1992 International Symposium on New Models for Software Architecture, Research Institute of Software Engineering, Tokyo, Japan, 1992, pp. 61–106.
[46] R. Milner, Communication and Concurrency, Prentice-Hall, 1989.
[47] M. Nesi, ”Mechanising a modal logic for value-passing agents in HOL,” in B. Steffen and D. Caucal (Eds.), Infinity’96, First International Workshop on Verification of Infinite State Systems, vol. 5 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. · Zbl 0912.68194
[48] M. Nesi, ”Formalising a value-passing calculus in HOL,” Formal Aspects of Computing, Vol. 11, pp. 160–199, 1999. · Zbl 0937.68112
[49] T. Nipkow, L.C. Paulson, and M. Wenzel, ”Isabelle/HOL: A Proof Assistant for Higher-Order Logic,” vol. 2283 of Lecture Notes in Computer Science, Springer, 2002. · Zbl 0994.68131
[50] G.D. Plotkin, ”A structural approach to operational semantics,” Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
[51] P. Rao, K. Sagonas, T. Swift, D.S. Warren, and J. Freire, ”XSB: A system for efficiently computing well-founded semantics,” in J. Dix, U. Furbach, and A. Nerode (Eds.), Proceedings of the 4th International Conference on Logic Programing and Nonmonotonic Reasoning, vol. 1265 of Lecture Notes in Artificial Intelligence, Springer, 1997, pp. 430–440.
[52] C. Röeckl, ”A first-order syntax for the {\(\pi\)}-calculus in Isabelle/HOL using permutations,” in S. Ambler, R. Crole, and A. Momigliano (Eds.), Proc. MERLIN’01, vol. 58.1 of Electronic Notes in Theoretical Computer Science, Elsevier, 2001. · Zbl 1268.68053
[53] C. Röeckl, ”On the mechanized validation of infinite-state and parameterized reactive, and mobile systems,” PhD thesis, Fakultät für Informatik, Technische Universität München, 2001.
[54] C. Röeckl, D. Hirschkoff, and S. Berghofer, ”Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the {\(\pi\)}-calculus and mechanizing the theory of contexts,” in F. Honsell and M. Miculan (Eds.), Proc. FOSSACS’01, vol. 2030 of Lecture Notes in Computer Science, Springer, 2001, pp. 364-378. · Zbl 0978.68045
[55] C. Sprenger, ”A verified model checker for the modal {\(\pi\)}-calculus in Coq,” in B. Steffen (Ed.), Tools 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, Proceedings, vol. 1384 of Lecture Notes in Computer Science, Springer, 1998, pp. 167-183.
[56] M.-O. Stehr and J. Meseguer, ”Pure type systems in rewriting logic,” in Proc. of LFM’99: Workshop on Logical Frameworks and Meta-Languages, Paris, France, 1999.
[57] C. Stirling, ”Modal and temporal logics for processes,” in F. Moller and G. Birtwistle (Eds.), Logics for Concurrency–Structure versus Automata (8th Banff Higher Order Workshop, August 27–September 3, 1995, Proceedings), vol. 1043 of Lecture Notes in Computer Science, Springer, 1996, pp. 149-237.
[58] D. Terrasse, ”Encoding natural semantics in Coq,” in V.S. Alagar (Ed.), Algebraic Methodology and Software Technology, 4th International Conference, AMAST ’95, Montreal, Canada, Proceedings, vol. 936 of Lecture Notes in Computer Science, Springer, 1995, pp. 230–244.
[59] A. Verdejo, ”CCS and LOTOS Semantics Implementation in Maude,” Web page. http://www.ucm.es/sip/alberto/ccs-lotos. · Zbl 1086.68552
[60] A. Verdejo, ”LOTOS symbolic semantics in Maude,” Technical Report 122-02, Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid, 2002. http://www.ucm.es/sip/alberto.
[61] A. Verdejo and N. Martí-Oliet, ”Implementing CCS in Maude,” in T. Bolognesi and D. Latella (Eds.), 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), Pisa, Italy, Kluwer Academic Publishers, 2000, pp. 351–366.
[62] S. Yu and Z. Luo, ”Implementing a model checker for LEGO,” in J. Fitzgerald, C. B. Jones and P. Lucas (Eds.), FME’97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997), vol. 1313 of Lecture Notes in Computer Science, Springer, 1997, pp. 442–458.
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.