© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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 kbytesBibtex 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},
}