School of Computing

Disjunction of LOTOS specifications

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

In T. Mizuno, N. Shiratori, T. Higashino, and A. Togashi, editors, Formal Description Techniques and Protocol Specification, Testing and Verification: FORTE X / PSTV XVII '97, pages 182-196, Osaka, Japan, November 1997. Chapman & Hall.

Abstract

LOTOS is a formal specification language, designed for the precise description of open distributed systems and protocols. The definition of, so called, implementation relations has made it possible also to use LOTOS as a specification technique for the design of such systems. These LOTOS based specification techniques usually (ab)use non-determinism to achieve implementation freedom. Unfortunately, this is unsatisfactory when specifying non-deterministic processes. We, therefore, propose to extend LOTOS with a disjunction operator in order to achieve more implementation freedom while maintaining the possibility to describe non-deterministic processes. In contrast with similar proposals we maintain the operational semantics. Download publication 67 kbytes

Bibtex Record

@inproceedings{350,
author = {M.W.A. Steen and H. Bowman and J. Derrick and E.A. Boiten},
title = {Disjunction of {LOTOS} specifications},
month = {November},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/350},
    address = {Osaka, Japan},
    booktitle = {Formal Description Techniques and Protocol Specification, Testing and Verification: FORTE X / PSTV XVII '97},
    editor = {T. Mizuno and N. Shiratori and T. Higashino and A. Togashi},
    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