Eventuality in LOTOS with a Disjunction Operator.pdf

Eventuality in LOTOS with a Disjunction Operator Yoshinao ISOBE, Yutaka SATO, Kazuhito OHMAKI Electrotechnical Laboratory 1-1-4 Umezono, Tsukuba, Ibaraki 305-8568, Japan E-mail:{ isobe|ysato|ohmaki }@etl.go.jp Abstract. LOTOS is a formal specification language, designed for the precise description of open distributed systems and protocols. Our pur- pose is to introduce the operators of logics (for example, disjunction, conjunction, greatest fixpoint, least fixpoint in μ-calculus) into (basic) LOTOS, in order to describe flexible specifications. Disjunction operators ∨ have been already proposed for expressing two or more implementa- tions in a flexible pecification. In this paper, we propose an extended LOTOS with two state operators. They can control recursive behavior, in order to express eventuality. The eventuality is useful for liveness prop- erties that something good must eventually happen. Then, we present a method for checking the consistency of a number of flexible specifications, and a method for producing a conjunction specification of them. 1 Introduction The design of large scale distributed systems is known to be a complex task. In order to support the design, formal description techniques (FDTs) are used for verifying that a realized system conforms to its specification. Process algebra such as CCS[12], CSP[4], and LOTOS[17] is one of FDTs, and especially LOTOS is standardized by ISO. In practise, flexible specifications are often given to a system instead of its complete specification in the first design step, and the flexible specifications are refined step by step, for reducing the number of possible implementations. In this case, a flexible specification represents two or more various implementations, however a specification described in process algebra usually represents only one implementation except equivalent implementations with it. In order to describe such flexible specifications, disjunction operators ∨ have been proposed by Steen et al.[