Semantic Refinement of Concurrent Object Systems Based on Serializability

The focus of our work is the object-oriented design and specification of distributed information systems applying the technique of stepwise refinement. Following the object-oriented paradigm, static and dynamic system properties have to be taken into account. The aspect of distribution brings in concurrency and communication. In this paper we formalize a refinement criterion for concurrent object systems which is inspired by the notion of serializable schedules as known from transaction processing theory. An object-oriented system specification determines the possible behaviour of the intended system. We use labelled event structures to model the concurrent behaviour of systems. For a correct refinement it is necessary that the abstract behaviour is represented in the refined model. At this point the idea of serialiazibility comes in. A concurrent abstract system run may be represented in the refined model by a sequential run as long as they have the same input/output behaviour. These refined runs can be characterized as serializable schedules. The work presented here is a first step towards bridging the gap between refinement of object-oriented specification concepts and database theory.