Starting B Specifications from Use Cases

Abstract

The B method is gaining visibility in formal methods com- munity due to excellent support for refinement. However, the traceability between the requirements and the formal model is still an issue of this method. On the other hand, use cases have become the informal industry standard for mapping functional requirements, describing the system's behavior using natural language. In this paper we show how controlled use cases can be used as a guideline for starting B specifications. In other words, our approach presents how a transaction, which is defined as an atomic part of the use case scenario, can be mapped as a B operation, providing a practical way to establish traceability between functional re- quirements and formal models.