Specification of Concurrent Objects

Concurrent objects are named concurrent processes that interact by invoking each other's operations. We describe how such concurrent objects can be specified, how objects can be composed, and how it can be shown that one object refines another.First a model is defined, based on a transition relation over two objects and an event. In the model, objects can be composed by parallel composition, encapsulation, and hiding of operations. Refinement between objects is defined as fair trace inclusion.A specification language is presented where objects can be specified operationally by abstract imperative programs as well as externally by formulas in an interval logic, and even in a combination of the two styles.Verification among the different specification styles is illustrated by a number of experiments using a small distributed data base as a common example. Also, experiments are made with the expressibility of the interval logic.