An Exercise in Formalising the Description of a Concurrent System

by David W. Bustard, Mark Norris, Rodney Orr and Adam C. Winstanley

Software - Practice and Experience, 22 (12), 1069-1098, December 1992.

ABSTRACT

LOTOS is one of the most recent formal description languages to appear and one of the 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 the use of other process-oriented notations such as CCS and CSP.