Object-Oriented Specifications of Distributed Systems in the μ-Calculus and Maude
Ulrike Lechner · Electronic Notes in Theoretical Computer Science · 1996
We refine an abstract property-oriented specification in the μ-calculus to a specification in Maude. As an intermediate step, we use a structured specification in the μ-calculus blended with propositions on states appropriate for object-oriented specification. We use the loose approach in refinement and refine data types as well as behavior. Throughout, our example is the bounded buffer.