An approach to developing modular specifications of distributed systems in Maude

An existing proposal for the separation of concerns in distributed systems provides a formal, object-based, layered approach for the composition of independent communication services. Compatible with that approach, a notion of service is introduced, which suggests not only the composition of independent layers, but also the refinement of specifications of distributed systems through composition of layers. An abstract layer is specified by combining computational and temporal logic specifications. A description is given of how it can be specified and model checked in Maude.