Providing concurrent implementations for Event-B developments

The Event-B method is a formal approach to modelling systems which incorporates the notion of refinement. This work bridges the abstraction gap between the lowest level of Event-B refinement and a working implementation. We focus on the link between Event-B and concurrent, object-oriented implementations and introduce an intermediate, object-oriented style specification notation called Object-oriented Concurrent-B (OCB). The OCB level of abstraction hides implementation details of locking and blocking, and provides the developer with a clear view of atomicity using labelled atomic clauses. OCB non-atomic clauses are given Event-B semantics, and OCB atomic clauses map to atomic events. Automatic translation of an OCB specification gives rise to an Event-B model and Java source code. The Java program will have atomicity that corresponds to the formal model (and therefore OCB clauses), and structure that is derived from the OCB model. We introduce process and monitor classes. Process classes allow specification of interleaving behaviour using non-atomic constructs, where atomic regions are defined by labelled atomic clauses. Monitor classes may be shared between the processes and provide mutually exclusive access to the shared data using atomic procedure calls. Labelled atomic clauses map to events guarded by a program counter derived from the label. This allows us to model the ordered execution of the implementation. The approach can be applied to object-oriented systems in general, but we choose Java as a target for working programs. Java's built-in synchronisation mechanism is used to provide mutually exclusive access to data. We discuss some problems related to Java programming, with regard to locking and concurrency, and their effect on OCB.The OCB syntax and mappings to Event-B and Java are defined, details of tool support and case studies follow. An extension to OCB is described in which a number of objects can be updated within a single atomic clause; facilitated by Java SDK 5.0 features. The extension allows direct access to variables of a monitor using dot notation, and multiple procedure calls in a clause. We also introduce new features to atomic actions such as a sequential operator, and atomic branching and looping