Behaviour specification of parallel active objects

The development of parallel programs is primarily concerned with application speed. This has led to the development of parallel applications in which software engineering aspects play only subordinate roles. In order to increase software quality in parallel applications, we motivate the construction of parallel programs by composing active objects which interact by means of an object-oriented coordination model. This paper presents a formalism for specifying the behaviour of parallel active objects and a corresponding notion of behavioural types which can be used for verifying whether certain active objects conform to a specified behaviour. Our approach is based on high-level Petri nets which enable (besides other benefits) automated analysis, in particular for automated type checking of active objects. We illustrate the usefulness of our approach by presenting reusable active objects for a manager/worker architecture. Their correct interaction is shown by automated checking of behavioural types. (C) 1998 Elsevier Science B.V. All rights reserved.status: publishe