Linking Event-B and Concurrent Object-Oriented Programs

The Event-B method is a formal approach to modelling systems, using refinement. Initial specification is a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. In software systems that use concurrent processing it is necessary to provide details of concurrent features before implementation. Our contribution is to show how Event-B models can be linked to concurrent, object-oriented implementations using an intermediate, object-oriented style specification notation. To validate our approach and gain further insight we automated the translation process with an Eclipse plug-in which produces an Event-B model and Java code. We call the new notation Object-oriented Concurrent-B (OC-B). The notation facilitates specification of the concurrent aspects of a development, and tes reasoning about concurrency issues in an abstract manner. We abstract away implementation details, such as locking, and provide the developer with a clear vie...

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Andrew Edmunds, Michael Butler
• Keywords: ENTCS 2008, Implementation, Object-oriented, Object-oriented Style Specification