Specifying, Analyzing and Programming Communication Systems in Maude

摘要

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.