Specifying, Analyzing and Programming Communication Systems in Maude

José Meseguer
Additional contact information
José Meseguer: SRI International

A chapter in Communication-Based Systems, 2000, pp 93-101 from Springer

Abstract: Abstract Rewriting logic is a logic well suited for the specification, prototyping, analysis, and programming of concurrent systems in which concurrent computation exactly corresponds to logical deduction. In particular, it can be used as a wide-spectrum semantic framework for communication systems. Being a semantic framework means that rewriting logic, instead of building in a particular model of concurrency or distribution, allows a wide range of such models to be specified as rewrite theories. As a wide-spectrum framework, it connects smoothly with notations suitable for the early phases of software design, from which one can pass to executable specifications written in rewriting logic that can then be formally analyzed in a variety of ways, including debugging, model checking, symbolic simulation, and theorem proving. Furthermore, one can then pass from executable specifications to efficient implementations by semantics-preserving transformations into subsets of the logic that are efficiently implementable as distributed or mobile languages. The paper summarizes the practical experience obtained so far by a number of authors in using the reflective rewriting logic language Maude to specify and analyze communication systems, and gives a brief sketch of Mobile Maude, an extension of Maude for secure mobile applications currently under development at SRI International.

Keywords: Model Check; Theorem Prove; Concurrent System; Mobile Object; Module Algebra (search for similar items in EconPapers)
Date: 2000
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-94-015-9608-4_7

Ordering information: This item can be ordered from
http://www.springer.com/9789401596084

DOI: 10.1007/978-94-015-9608-4_7

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().