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.

A formal framework for viewpoint consistency. H. Bowman, M.W.A. Steen, E.A. Boiten, and J. Derrick. Computing Laboratory Technical Report 22-99, University of Kent at Canterbury, Canterbury, Kent, CT2 7NZ, December 1999, to appear in Formal Methods in System Design.
Strategies for consistency checking based on unification. H. Bowman, E. A. Boiten, J. Derrick, and M. W. A. Steen. Science of Computer Programming, 33:261-298, April 1999.
Viewpoint consistency in ODP, a general interpretation. H. Bowman, E. Boiten, J. Derrick, and M. Steen. In E. Najm and J.-B. Stefani, editors, First IFIP International Workshop on Formal Methods for Open Object-Based Distributed Systems, pages 189-204. Chapman & Hall, March 1996.
Cross viewpoint consistency in Open Distributed Processing. H. Bowman, J. Derrick, P. Linington, and M. Steen. Software Engineering Journal, 11(1):44-57, January 1996.

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.

Consistency of partial process specifications. Maarten Steen, John Derrick, Eerke Boiten, and Howard Bowman. In Armando Haeberer, editor, AMAST'98, page 15. Springer Verlag, January 1999.
Disjunction of LOTOS specifications. M.W.A. Steen, H. Bowman, J. Derrick, and E.A. Boiten. In T. Mizuno, N. Shiratori, T. Higashino, and A. Togashi, editors, Formal Description Techniques and Protocol Specification, Testing and Verification: FORTE X / PSTV XVII '97, pages 177-192, Osaka, Japan, November 1997. Chapman & Hall.

The following publication presents some early, but still relevant, ideas on consistency in LOTOS.

Composition of LOTOS specifications. M. W. A. Steen, H. Bowman, and J. Derrick. In P. Dembinski and M. Sredniawa, editors, Protocol Specification, Testing and Verification, XV, pages 73-88, Warsaw, Poland, January 1995. Chapman & Hall.

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.

Constructive consistency checking for partial specification in Z. E.A. Boiten, J. Derrick, H. Bowman, and M.W.A. Steen. Science of Computer Programming, 35(1):29-75, September 1999.

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.

Viewpoint consistency in Z and LOTOS: A case study. E. Boiten, H. Bowman, J. Derrick, and M. Steen. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science, pages 644-664. Springer-Verlag, September 1997.
Translating LOTOS to Object-Z. J. Derrick, E.A. Boiten, H. Bowman, and M. Steen. In D.J. Duke and A.S. Evans, editors, Northern Formal Methods Workshop, volume 2nd BCS-FACS Northern Formal Methods Workshop of Workshops in Computing. Springer-Verlag, July 1997.

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.