Rewriting logic seems very well suited as a semantic framework for open object-based distributed systems. Both the distributed states and the local concurrent transitions of such systems can be naturally specified by rewrite theories in which such local concurrent transitions are described by rewrite rules. Maude is a high-performance rewriting logic language and system developed at SRI International that supports executable specification and programming, and a flexible variety of formal analyses. As a wide-spectrum semantic framework, rewriting logic can span the gap between high-level properties and architectural designs on the one hand, and distributed or mobile system implementations on the other. Rewriting logic has been used to give a precise semantics to a number of distributed architectural notations and to obtain formal executable specifications from them. Using Maude and its associated tools, such executable specifications can then be formally analyzed in a variety of ways. Furthermore, high-level properties of such specifications expressed in nonexecutable formalisms such as temporal and modal logics can likewise be analyzed and verified. Since under quite reasonable assuptions rewriting logic specifications can be directly implemented as distributed and mobile systems, it is possible to span the gap from high-level designs to implementations without leaving the formal framework. This paper introduces rewriting logic and Maude, and surveys the experience that, thanks to the efforts of several research teams, has been gained so far in applying them to open object-based distributed systems.
展开▼
