A Use Case Interpretation of B AMN

In this paper we suggest methods to aid the development of specifications using the B method. We propose an objectoriented approach to specification, developing the structure through refinement. We start with a use case analysis to find the functionality of the system, and then use a number of objects to specify the use case in greater detail. We separate data, interface and behavioural aspects of the specification in order to minimise changes in the problem domain. We illustrate the method using a simple case study, and discuss other object-oriented concepts such as components and design patterns.