Derrick, J. and Boiten, E.A. and Bowman, H. and Steen, M. (1999) Viewpoints and consistency: translating LOTOS to Object-z. Computer Standards & Interfaces, 21 (3). pp. 251-272. ISSN 0920-5489.
This paper presents a translation between the formal description technique LOTOS and the object-oriented specification language Object-Z. The need for such a translation lies in the use of formal methods in viewpoint specification, and in particular in the Open Distributed Processing standard. The use of viewpoints as a set of partial interlocking specifications brings an obligation to check the consistency of these partial specifications, and to do so we need to relate specifications written in differing languages. The work presented here aims to support the consistency checking of viewpoints written using formal methods by defining a translation from LOTOS to Object-Z. A LOTOS specification describes both an ADT component and a behavioural model, the former is translated into the Z type system, and the behavioural specification is translated into a collection of Object-Z classes where we relate LOTOS actions to operations in the Object-Z specification. A case study is presented which illustrates the translation and consistency checking techniques discussed in the paper.
|Uncontrolled keywords:||distributed systems; open distributed processing; formal methods (Object-z, LOTOS); viewpoints; consistency; partial specification|
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing|
|Depositing User:||M. Nasiriavanaki|
|Date Deposited:||21 Jun 2009 21:55|
|Last Modified:||06 Sep 2011 02:19|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/17284 (The current URI for this page, for reference purposes)|
- Depositors only (login required):