On message specifications in OCL

Abstract

The object constraint language (OCL) is the established language for specifying of properties of objects and object structures. Recently an extension of OCL has been proposed for the specification of messages sent between objects. In this paper we present a generalization of this extension which allows additionally to specify causality constraints. From a pragmatic point of view, such causality constraints are needed to express, for example, that each acknowledgment must be preceded by a matching request, which is frequently required by communication protocols. Our generalization is based on the introduction of histories into OCL. Histories describe the external behavior of objects and groups of objects. Moreover, to reason compositionally about the behavior of a complex system we distinguish between local specifications of a single object and global specifications describing the interaction between objects. These two types of specifications are expressed in syntactically different dialects of OCL. Our notion of compositionality, which is formalized in this paper by a compatibility predicate on histories, allows the verification of models during the early stages of a design.