FORMOSA (Formalisation of ODP Systems Architecture)
IntroductionThis 36-month project was funded by EPSRC under grant J17555, ending in October 1996. The objectives of the project were briefly:
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 SemanticsArchitectural 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 ConceptsThe 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 ConceptsSelected 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 SemanticsThe 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 PublicationsSee 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