School of Computing

Comparing LOTOS and Z refinement relations

J. Derrick, H. Bowman, E.A. Boiten, and M. Steen

In FORTE/PSTV'96, pages 182-196, Kaiserslautern, Germany, October 1996. Chapman & Hall.


This paper compares the LOTOS and Z refinement relations. The motivation for such a comparison is the use of multiple viewpoints for specifying complex systems defined by the reference model of the Open Distributed Processing (ODP) standardization initiative.

The ODP architectural semantics describes the application of formal description techniques (FDTs) to the specification of ODP systems. Of the available FDTs, Z is likely to be used for at least the information, and possibly other, viewpoints, whilst LOTOS is a strong candidate for use in the computational viewpoint. Mechanisms are clearly needed to support the parallel development, and integration of, viewpoints using these FDTs. We compare the LOTOS bisimulation relations and the reduction relations to the Z refinement relation showing that failure-traces refinement corresponds closely to refinement in Z.

Download publication 108 kbytes

Bibtex Record

author = {J. Derrick and H. Bowman and E.A. Boiten and M. Steen},
title = {Comparing {LOTOS} and {Z} refinement relations},
month = {October},
year = {1996},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    ISBN = {0 412 79490 X},
    address = {Kaiserslautern, Germany},
    booktitle = {FORTE/PSTV'96},
    publisher = {Chapman & Hall},
    refereed = {yes},

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

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

Last Updated: 21/03/2014