An Exercise in Formalizing the Description of a Concurrent System

LOTOS is one of the most recent formal description languages to appear and one of very few with a standard definition. It has both a process algebra and an abstract data-type component, and these facilities are used in combination to describe the behaviour of concurrent systems. The purpose of this paper is to examine, in a tutorial style, what is involved in constructing and taking benefit from such descriptions. The presentation is illustrated through the development of two formal descriptions for the children’s game of pass-the-parcel. These descriptions and a concise summary of the main features of LOTOS are given as appendices. Many of the points made in the paper apply equally well to other process-oriented languages such as CCS and CSP