School of Computing

Viewpoints and consistency: translating LOTOS to Object-Z

John Derrick, Eerke Boiten, Howard Bowman, and Maarten Steen

Computer Standards and Interfaces, 21:182-196, August 1999.

Abstract

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.

Download publication 302 kbytes (PostScript)

Bibtex Record

@article{954,
author = {John Derrick and Eerke Boiten and Howard Bowman and Maarten Steen},
title = {Viewpoints and consistency: translating {LOTOS}  to {O}bject-{Z}},
month = {August},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/954},
    journal = {Computer Standards and Interfaces},
    publication_type = {article},
    publisher = {Elsevier},
    submission_id = {4153_947787372},
    volume = {21},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014