School of Computing

Composition of LOTOS specifications

M. W. A. Steen, H. Bowman, and J. Derrick

In P. Dembinski and M. Sredniawa, editors, Protocol Specification, Testing and Verification, XV, pages 182-196, Warsaw, Poland, January 1995. Chapman & Hall.


Usually formal methods adopt the traditional waterfall model of system design. New design methodologies, such as Open Distributed Processing and Object Oriented Design, allow for incremental and partial specification. In order to support such design methods, the issues of consistency between specifications and composition of (partial) specification become vital. This paper presents a general framework for dealing with partial specification, which is instantiated for the specification language LOTOS. Necessary and sufficient conditions for consistency to hold between LOTOS specifications are given, and an operational semantics for composition is proposed.

Keywords: LOTOS, formal methods, consistency, composition, incremetal specification, refinement.

Bibtex Record

author = {M. W. A. Steen and H. Bowman and J. Derrick},
title = {Composition of {LOTOS} specifications},
month = {January},
year = {1995},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    address = {Warsaw, Poland},
    booktitle = {Protocol Specification, Testing and Verification, XV},
    editor = {P. Dembinski and M. Sredniawa},
    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