The influence of the formal description technique LOTOS on concurrent system design

In this paper we investigate the applicability of the formal description language LOTOS for specifying a concurrent system. We are particularly interested in how a specifier might capture a system's requirements, given LOTOS as a choice of target formal description language. We show how a LOTOS specification can be modularised using encapsulated processes. A simple case study is introduced, specified using LOTOS. Questions about different design issues concerning process composition with regard to capturing the required behaviour of the case study system are then raised, together with possible solutions.