Abstract
I will introduce the main ideas of rewriting logic [11]—a logic for the specification, prototyping and programming of concurrent systems in which concurrent computation exactly corresponds to logical deduction—and will discuss some promising directions for its use as a logical and semantic framework for distributed computing and communication protocols. An important aspect is its wide-spectrum character. Thus, on the one hand it connects smoothly with—and provides a formal foundation for—notations suitable for the early phases of software design, such as architectural description languages and object-oriented modeling languages [14, 19]; and on the other hand it also provides a natural implementation path through subsets of the logic that are efficiently implement able as distributed or mobile languages [9]. Similarly, rewriting logic specifications, when supported by appropriate tools, can be used in a wide range of specification, prototyping, code generation, testing, formal analysis, and formal verification efforts to reach high levels of assurance about a system’s correctness. All these capabilities seem potentially useful for specifying, prototyping, testing, validating, and implementing distributed systems in general and communication protocols in particular; and they offer the promise of substantially narrowing the gap between specification and code. and of reaching high assurance about the correctness of implementations that can themselves be realized in efficient subsets of rewriting logic.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35394-4_29
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. Bergstra and J. Tucker. Characterization of computable data types by means of a finite equational specification method. In J. W. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming, Seventh Colloquium, pages 76–90. Springer-Verlag, 1980. LNCS, Volume 81.
M. Clavel. Reflection in general logics and in rewriting logic, with applications to the Maude language. Ph.D. Thesis, University of Navarre, 1998.
M. Clavel, F. Duran, S. Eker, and J. Meseguer. Building equational logic tools by reflection in rewriting logic. In Proc. of the CafeOBJ Symposium ‘88, Numazu, Japan. CafeOBJ Project, April 1998.
M. Clavel, F. Duran, S. Eker, J. Meseguer, and P. Lincoln. An introduction to Maude (beta version). Manuscript, SRI International, March 1998.
M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm.
M. Clavel and J. Meseguer. Reflection and strategies in rewriting logic. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm.
G. Denker, J. Meseguer, and C. Talcott. Protocol Specification and Analysis in Maude. In N. Heintze and J. Wing, editors, Proc. of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana, 1998.
C. Kirchner and H. Kirchner (eds.). Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications, ENTCS, North Holland, 1998.
P. Lincoln, N. Marti-Oliet, and J. Meseguer. Specification, transformation, and programming of concurrent systems in rewriting logic. In G. Blelloch, K. Chandy, and S. Jagannathan, editors, Specification of Parallel Algorithms, pages 309–339. DIMACS Series, Vol. 18, American Mathematical Society, 1994.
N. Marti-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwi.elsevier.nl/mcs/tcs/pc/volume4.htm.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96 (1): 73–155, 1992.
J. Meseguer. Rewriting logic as a semantic framework for concurrency: a progress report. In Proc. CONCUR’96, Pisa, August 1996, pages 331–372. Springer LNCS 1119, 1996.
J. Meseguer. Research directions in rewriting logic. In U. Berger and H. Schwichtenberg, editors, Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 - August 6, 1997. Springer-Verlag, 1998.
J. Meseguer and C. Talcott. Using rewriting logic to interoperate architectural description languages (I and II). Lectures at the Santa Fe and Seattle DARPA-EDCS Workshops, March and July 1997. http://www-formal.stanford.edu/c1t/ArpaNsf/adl-interop.html.
E. Najm and J.-B. Stefani. Computational models for open distributed systems. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-based Distributed Systems, Vol. 2, pages 157–176. Chapman and Hall, 1997.
S. Nakajima. Encoding mobility in CafeOBJ: an exercise of describing mobile code-based software architecture. In Proc. of the CafeOBJ Symposium ‘88, Numazu, Japan. CafeOBJ Project, April 1998.
I. Pita and N. Marti-Oliet. A Maude specification of an object oriented database model for telecommunication networks. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwi.elsevier.nl/mcs/tcs/pc/volume4.htm.
C. L. Talcott. An actor rewrite theory. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications,volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm.
M. Wirsing and A. Knapp. A formal approach to object-oriented software engineering. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications,volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Meseguer, J. (1998). A Logical Framework for Distributed Systems and Communication Protocols. In: Budkowski, S., Cavalli, A., Najm, E. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. PSTV FORTE 1998 1998. IFIP — The International Federation for Information Processing, vol 6. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35394-4_20
Download citation
DOI: https://doi.org/10.1007/978-0-387-35394-4_20
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5262-5
Online ISBN: 978-0-387-35394-4
eBook Packages: Springer Book Archive