Viewpoint Specification using Formal Methods

Viewpoint Specification using Formal Methods

Howard Bowman

Specification by viewpoints is widely advocated as a useful method for dealing with the complexity of large systems. Each viewpoint describes an aspect (rather than a component or module) of the envisaged system, using a language most suited to the viewpoint at hand. A consequence of adopting such an approach is that descriptions of the same or related entities can appear in different viewpoints and must co-exist. Thus, consistency of specifications across viewpoints becomes a central issue.

I have worked on this topic with a number of other people, in particular, Eerke Boiten, John Derrick, Peter Linington, and Maarten Steen. This work was mainly performed within the bounds of the (now finished) EPSRC funded Project Cross Viewpoint Consistency in Open Distributed Processing; a more extensive description of which can be found at the project home page.

The particular viewpoints model that inspired this project was that included in the Open Distributed Processing Reference Model (ODP), which is an architecture for modelling and constructing open distributed systems. The architecture has been standardised by the International Standards Organization

Our work on this topic can be presented under five headings:

Framework for Viewpoint Consistency

Our "framework" papers define the formal concepts underlying consistency checking. They give a general interpretation of consistency in terms of the existence of a common development of the viewpoint specifications and they investigate the feasibility of checking this notion of consistency. In particular, a number of different classes of consistency are highlighted and the relative feasibility of consistency checking within these different classes is considered.

The following four papers are all centred on our framework for cross viewpoint consistency. The first is probably the most complete presentation of the framework. Although Maarten Steen's PhD thesis also makes important contributions to the definition of a formal framework for consistency.

Consistency in LOTOS

Our work on LOTOS considers how multiple specifications written in the LOTOS formal specification notation can be checked for consistency. The most comprehensive text on this material is Maarten Steen's PhD thesis. However, the following publications are also available.

The following two publications summarise some of the main ideas of Maarten's thesis.

The following publication presents some early, but still relevant, ideas on consistency in LOTOS. Some other early ideas of ours on consistency in LOTOS can be found in the framework papers in the previous section.

Consistency in Z

Within the auspices of the Cross Viewpoint Consistency in ODP project we have also extensively investigated how to check consistency between pairs of Z specifications. The following paper highlights the main elements of our work on this topic. However, a number of other publications can be found on the Cross Viewpoint Consistency in ODP home page.

Consistency between LOTOS and Z

Since different languages and techniques can be used in different viewpoints, yielding a multi-paradigm approach to system development, it is necessary to relate different formal notations. In order to investigate the feasibility of relating viewpoint specifications written in different notations we considered how LOTOS specifications can be translated into Z, thus, enabling consistency checking to be performed in Z.

Once again, we have written a number of papers on this topic and the most comprehensive source for these publications is the Cross Viewpoint Consistency in ODP home page. However, the following two papers summarise the main ideas.

Resulting Research Directions

The original Cross Viewpoint Consistency in ODP project is now finished. However, a number of directions for further research have spun-off from this project, e.g. Some of this work is being pursued within the follow-up EPSRC project OpenViews.

Back to Howard Bowman's home page.

Last modified December 1999.