This is a companion site to our work on bringing compositional specification and verification to rewriting logic and Maude.
Please, send any comments to omartins at ucm dot es.
| Status: | Sent to be considered for publication. | |
| Abstract: | In previous work, summarized in this paper, we proposed an operation of composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present paper focuses on compositional verification. We show how the assume/guarantee technique can be transposed to our setting, by giving appropriate definitions of satisfaction based on transition structures and path semantics. We also show that simulation and equational abstraction can be done componentwise. Our composition operation is rather lax, in the sense that it allows and requires a discussion on the appropriate concepts of fairness and deadlock as they affect satisfaction of temporal properties. We keep at all times in parallel a distributed and a global view of composed systems. We show that these views are equivalent and interchangeable, which may help our intuition and also has practical uses as, for example, it allows global-style verification of a modularly modeled system. | |
| Artifacts: | See below the artifacts from the Python implementation. In particular, inside the zipped file with the examples, the ones used in this paper are in the files buffers.cmaude, mutex.cmaude, and river.cmaude. Also the additional and more complex examples mentioned in the paper are in the files abp.cmaude and nspkp.cmaude. |
| Status: | Functional, but not a polished tool at present. | |
| Description: | The implementation is to be fed with a specification written in the extension of the Maude language that we sketched in our paper Compositional specification in rewriting logic and we fully describe in the upcoming PhD thesis. It produces an equivalent standard Maude specification. The original specification can include assume/guarantee assertions and, then, the translation includes the LTL formulas that need to be verified on each component system. | |
| Artifacts: | Python source code (zipped) Example systems (zipped) User manual and other docs (zipped) |
| Status: | Successfully defended on Sep 2021. | |
| Abstract: | In short, this thesis shows that compositional specification and verification are doable in rewriting logic and in Maude if they are enriched with appropriate extensions. | |
| Artifacts: | Thesis |
| Status: | Presented at WRLA 2021 (held online) as work in progress. | |
| Abstract: | Our goal is finding ways to perform compositional verification of systems specified in rewriting logic and Maude. In previous work, we described a means for compositional specification in rewriting logic; this paper continues that work and is based on it. Although some theoretical developments have been needed, our main goal is not creating new techniques, but showing how to adapt existing ones to our setting. We study, in particular, the assume/guarantee technique, and component-wise simulation and equational abstraction. We hope these show the way to adapting other techniques that may be more suitable in each case. A toy example shows how they can be used in practice. | |
| Artifacts: | Live recording of online presentation (video) |
| Status: | Published in 2020 in TPLP. | |
| Abstract: | 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. | |
| Artifacts: | TPLP paper |
| Status: | Presented at WRLA 2018. Published in LNCS 11152. | |
| Abstract: | 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. | |
| Artifacts: | LNCS paper Completely specified example on ABP (PDF) Recorded replay of WRLA 2018 presentation (Youtube video) |
| Status: | Presented at ATVA 2016. Published in LNCS 9938. | |
| Abstract: | 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. | |
| Artifacts: | LNCS paper Extended version of paper (PDF) Slides from ATVA 2016 (PDF) Maude implementation and examples (zipped) |
| Status: | Presented at WRLA 2016. Published in LNCS 9942. | |
| Abstract: | We argue that considering transitions at the same level as states, as first-class citizens, is advantageous in many cases. Namely, the use of atomic propositions on transitions, as well as on states, allows temporal formulas and strategy expressions to be more powerful, general, and meaningful. We define "egalitarian" structures and logics, and show how they generalize well-known state-based, event-based, and mixed ones. We present translations from egalitarian to non-egalitarian settings that, in particular, allow the model checking of LTLR formulas using Maude's LTL model checker. We have implemented these translations as a prototype in Maude itself. | |
| Artifacts: | LNCS paper Extended version of paper (PDF) Slides from WRLA 2016 (PDF) Maude implementation and examples (zipped) |