|
The aim of this project is to develop techniques that enable the consistency of specifications in the Open Distributed Processing (ODP) Model to be maintained. The project will develop a formal framework for consistency in ODP and will realise this framework by building a prototype tool set for checking the consistency of ODP specifications. Techniques for consistency checking between Z and LOTOS, which are two of the most important FDTs used in ODP, will be focused on. It is envisaged that the development of such techniques will act as a significant verification of concept for the full ODP consistency problem. The results of the research will be fed back into the ODP standardisation activities.Progress:ODP is a natural progression from OSI, broadening the target of standardisation from the point of interconnection to the end-to-end system behaviour. One of the cornerstones of ODP is a model of multiple viewpoints which enables different participants to observe a system from a suitable perspective and at a suitable level of abstraction. The practicalities of how to make this approach work are only beginning to be explored. In particular, one of the consequences of adopting a multiple viewpoint approach to development is that descriptions of the same or related objects can appear in different viewpoints and must co-exist. Furthermore, different notations are likely to be used in different viewpoints. Consistency of of specifications across viewpoints thus becomes a central issue. The project has only just officially began, however, our work to date has suggested that satisfactory consistency relationships between specifications in the same FDT can be located. Specifically, we have discovered suitable intra language consistency relationships for both Z and LOTOS, these are reported in [1,2,3]. Furthermore, algorithms which enable pairs of specifications to be combined (called unification) have also been developed for Z and LOTOS. We are currently seeking to realise these intra language consistency relationships by developing prototype consistency checking tools for Z and LOTOS. We are initially focusing on developing a unifier for Z, which will build upon Logicas Z tool Formalizer. This tool will work with a second prototype tool which will check that the unified specification is free from contradictions and can thus be implemented. This second tool will build upon well understood theorem proving technology. Inter language unification and consistency checking, which involves the very difficult area of translation across FDT families, will be the focus of the final phase of this project. We believe that this research is timely and of great importance since without a realistic approach to maintaining the consistency of specifications across multiple viewpoints the potential of the existing and ongoing work on the ODP model cannot be fully realised. [1] Bowman, H., J. Derrick and M. Steen Some Results on Cross Viewpoint Consistency Checking ICODP'95, IFIP International Conference on Open Distributed Processing, Publisher: North-Holland, Brisbane, Australia, February 1995.[2] Bowman, H., J. Derrick, P.F. Linington and M. Steen FDTs for ODP Computer Standards and Interfaces, Special Issue on Formal Methods in Standards, Editor of Special Issue: H. Kilov, To Appear September 1995.[3] Derrick, J., H. Bowman and M. Steen Maintaining Cross Viewpoint Consistency Using Z ICODP'95, IFIP International Conference on Open Distributed Processing, Publisher: North-Holland, Brisbane, Australia, February 1995. BT research labs and APM Ltd Cambridge are collaborating on this project.
|