FORMOSA (Formalisation of ODP Systems Architecture)

Introduction

This 36-month project was funded by EPSRC under grant J17555, ending in October 1996. The objectives of the project were briefly:

• to support the development of standards for ODP (Open Distributed Processing)
• to improve the quality of these standards
• to effectively exploit the formal techniques LOTOS and Z in standardising ODP
• to define LOTOS and Z architectural semantics for ODP.

The project was undertaken at Stirling by Richard Sinnott under the supervision of Ken Turner. The project was collaborative, with Steve Rudkin of British Telecommunications PLC as project manager. Other technical contributions were made by Jonathan Legh-Smith and Pete Young of BT. The University of Kent contributed to a separate but related project on cross-viewpoint consistency in ODP. The participants from UKC in this were Howard Bowman, John Derrick and Maarten Steen.

ODP Architectural Semantics

Architectural semantics serves as a bridge between the concepts of an architecture and the concepts of a specification language. Architectural semantics allows architectural concepts to be formalised, and gives an architectural interpretation to a formal specification. An architectural semantics is important for ensuring consistent formalisation of standards for an architecture. It also ensures that formal specifications of different standards can be related to each other, even if they are written in different languages. A mixture of prescriptive and descriptive styles was adopted according to the ODP concepts being formalised. Stirling provided the editor for the architectural semantics standard (ISO/IEC 10746-4) developed largely by the project.

ODP Foundation Concepts

The project developed an architectural semantics for the foundation concepts given in Part 2 of the ODP Reference Model. The LOTOS formalisation was fairly straightforward, though there were many detailed modelling issues to be investigated. The experience gained from using LOTOS was then applied to defining the foundation concepts in Z. The main obstacle was that `standard' Z does not really have the concept of object. Standard LOTOS is not object-oriented either, though it can be used in this way. The project developed a style for using Z to capture object-oriented aspects of ODP.

ODP Architecture Concepts

Selected languages from Part 3 of the ODP Reference Model were also specified: the enterprise, information and computational viewpoints. LOTOS proved appropriate for describing the computational viewpoint, largely because both are fairly operational. Z was less successful for this because it is more abstract and lacks an accepted object-oriented style. Despite this, a usable Z approach was developed for modelling the computational viewpoint. When the enterprise and information viewpoints were investigated, the suitability of LOTOS and Z was found to be reversed. Z lent itself better to higher-level concepts while LOTOS forced a rather descriptive style of specification.

Application of Architectural Semantics

The formalisation of ODP foundation and architecture concepts was put to use on a real application. A specification was developed in LOTOS of the ODP trader. This was supplemented by studies of type management using LOTOS and Z. The LOTOS approach was not very satisfying since types and processes are second-class citizens in the language. Z was much more effective, and was also used to specify multimedia binding issues. A complete type model was developed for ODP using Z. This handles the different roles of types when interfaces are bound or substituted for each other. It also extends the basic syntactic aspects of type checking in ODP to include behavioural considerations and non-functional issues.

Project Publications

See the final report for a fuller description of the results. Links in the following publications list point to PostScript files which need gunzip to be decompressed.

Richard O. Sinnott. The development of an architectural semantics for ODP. Technical Report CSM-121, Department of Computing Science and Mathematics, University of Stirling, UK, March 1994.

Richard O. Sinnott. The formal specification in LOTOS of a basic type manager. Technical Report CSM-122, Department of Computing Science and Mathematics, University of Stirling, UK, April 1994.

Richard O. Sinnott, editor. Open Distributed Processing - Basic Reference Model - Part 4: Architectural Semantics. ISO/IEC DIS 10746-4, November 1996.

Richard O. Sinnott, editor. Open Distributed Processing - Basic Reference Model - Part 4: Architectural Semantics Amendment. ISO/IEC DIS 10746-4.1, November 1996.

Richard O. Sinnott and Kenneth J. Turner. Modelling ODP viewpoints. In B. Cameron, C. Geldrez, A. Hopley, D. Howes, B. Mirek, and M. Plucinska, editors, Proc. OOPSLA 94 Workshop on Precise Behavioural Specifications in OO Information Modelling, pages 121-128, Portland, Oregon, USA, October 1994.

Richard O. Sinnott and Kenneth J. Turner. Applying formal methods to standard development: The Open Distributed Processing experience. Computer Standards and Interfaces, 17:615-630, October 1995.

Richard O. Sinnott and Kenneth J. Turner. Specifying ODP computational objects in Z. In Elie Najm and Jean-Bernard Stefani, editors, Proc. Formal Methods for Open Object Based Distributed Systems, pages 391-406, Paris, March 1996. Ecole Nationale Supérieure des Télécommunications, ENST 96S001.

Richard O. Sinnott and Kenneth J. Turner. Specifying multimedia binding objects in Z, Proc. Workshop on Trends in Distributed Systems, Aachen, Germany, October 1996.

Richard O. Sinnott and Kenneth J. Turner. Applying the architectural semantics of ODP to develop a trader specification (pre-publication version). Computer Networks and ISDN Systems, March 1997.

Richard O. Sinnott and Kenneth J. Turner. Type checking in distributed systems: A complete model and its Z specification, Proc. Int. Conf. on Open Distributed Processing, Toronto, Canada, May 1997.

Kenneth J. Turner. Specification architecture illustrated in a communications context (pre-publication version). Computer Networks and ISDN Systems, March 1997.

Kenneth J. Turner. Relating architecture and specification (pre-publication version). Computer Networks and ISDN Systems, March 1997.

Kenneth J. Turner and Marten van Sinderen. LOTOS specification style for OSI. In Tommaso Bolognesi, Jeroen van de Lagemaat and Chris A. Vissers, editors, The LOTOSPHERE Project, pages 137-159. Kluwer Academic Publishers, London, UK, 1995.

Up one level to Ken Turner - Research Projects