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 177-192, 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 = {177-192},
keywords = {LOTOS, process algebra, specification, disjunction,  operational semantics},
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},
}