Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. We discuss the motivations and implications of our proposal, formalize it for rewriting logic and also for transition structures, to be used as semantics, and show the power of our approach with some examples. This paper is under consideration in Theory and Practice of Logic Programming (TPLP).
Our paper @cite_5 contains a first definition of the synchronous composition of rewrite systems. There, we proposed to synchronise the execution of rules from different systems based on the coincidence of (atomic) rule labels. This reflects the synchronisation of actions in process algebras and in automata, for example. We also proposed to synchronise states by agreement on the Boolean values of propositions defined on them. We implemented that concept of synchronisation on Maude. That proposal had the advantage that it used standard machinery already existing in Maude: rule labels are basic elements of Maude's syntax, and propositions are customarily defined and used to build LTL formulas to be used with Maude's model checker. Why is the present, much more involved paper needed? We refer the reader to . In short: Boolean-valued propositions are not enough to allow flexible synchronisation and value-passing; we need to give more substance to transitions; we want to be able to synchronise an action at one system with several consecutive ones at the other system. A complex realistic example like the one on the alternating bit protocol in @cite_33 would not be possible in our previous setting.
@cite_5 @cite_33
2521108378 2890370072
We present a concept of module composition for rewrite systems that we call synchronous product, and also a corresponding concept for doubly labeled transition systems (as proposed by De Nicola and Vaandrager) used as semantics for the former. In both cases, synchronization happens on states and on transitions, providing in this way more flexibility and more natural specifications. We describe our implementation in Maude, a rewriting logic-based language and system. A series of examples shows their use for modular specification and hints at other possible uses, including modular verification. Our overall goal is compositional specification and verification in rewriting logic. In previous work, we described a way to compose system specifications using the operation we call synchronous composition. In this paper, we propose the use of parameterized programming to encapsulate and handle specifications: theories represent interfaces; modules parameterized by such theories instruct on how to assemble the parameter systems using the synchronous composition operation; the implementation of the whole system is then obtained by instantiating the parameters with implementations for the components. We show, and illustrate with examples, how this setting facilitates compositionality.