© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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 182-196. Springer-Verlag, September 1997.Abstract
Specification by viewpoints is advocated as a suitable method of specifying complex systems. Each viewpoint describes the envisaged system from a particular perspective, using concepts and specification languages best suited for that perspective.
Inherent in any viewpoint approach is the need to check or manage the consistency of viewpoints and to show that the different viewpoints do not impose contradictory requirements. In previous work we have described a range of techniques for consistency checking, refinement, and translation between viewpoint specifications, in particular for the languages LOTOS and Z. These two languages are advocated in a particular viewpoint model, viz. that of the Open Distributed Processing (ODP) reference model. In this paper we present a case study which demonstrates how all these techniques can be combined in order to show consistency between a viewpoint specified in LOTOS and one specified in Z.
Keywords: Viewpoints; Consistency; Z; LOTOS; ODP.
Download publication 87 kbytesBibtex Record
@conference{182, author = {E. Boiten and H. Bowman and J. Derrick and M. Steen}, title = {Viewpoint consistency in {Z} and {LOTOS}: A case study}, month = {September}, year = {1997}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1997/182}, Editor = {J. Fitzgerald and C.B. Jones and P. Lucas}, ISBN = {3-540-63533-5}, booktitle = {FME'97: Industrial Applications and Strengthened Foundations of Formal Methods}, publisher = {Springer-Verlag}, refereed = {yes}, series = {Lecture Notes in Computer Science}, volume = {1313}, }