Formalizing ODP computational viewpoint specifications in Maude

The ODP computational viewpoint describes the functionality of a system and its environment, in terms of a configuration of objects which interact at interfaces. Computational objects provide a functional decomposition of the system, independently of its distribution. Although several notations have been proposed to model this ODP viewpoint, either they are not expressive enough to faithfully represent all its concepts, or they tend to suffer from a lack of formal support. We explore the use of Maude as a formal notation for writing ODP computational viewpoint specifications. Maude is an executable rewriting logic language specially well suited for the specification of object-oriented open and distributed systems. We show how Maude offers a simple, natural, and accurate way of modelling the ODP computational viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.