Full text: Download
The formal specification language LOTOS is an international standard for use in Open Systems Interconnection. A timed extension called ET-LOTOS has been proposed. This paper presents a fully-abstract denotational semantics for the process algebraic component of this extension. The benefits of a denotational semantics are discussed, as are the applications. 1 Introduction LOTOS is a language intended primarily for use in protocol specification. It is a synthesis of two process calculi---CCS [9] and CSP [4]---with the addition of data types. It is an international standard for use in Open Systems Interconnection [5], and has been used to specify a wide variety of information processing systems [12]. LOTOS is about to undergo its first major revision. It is to be extended to include an explicit treatment of time. In [7], the authors introduce a language called ET-LOTOS. They extend the standard language by giving a timed interpretation to existing operators and adding new operators to mo...