Starting B specifications from use cases

Abstract

The B method [1] is gaining visibility in formal methods community due to excellent support for refinement. However, the traceability between the requirements and the formal model is still an issue of this method. To overcome this issue, different solutions have been proposed by researchers. In [2], the authors have presented a traceability between KAOS requirements and B. A mixed solution using natural language and UML-B has been proposed by [3]. However, these approaches use non-standard artifacts for requirement specifications, which we consider a disincentive for convincing designers to adopt formal methods since they must spend time to learn them. So, we propose an approach for mapping requirements to B models from use cases [4], which can be considered as the de-facto industry standard for requirement specifications. We propose that use case scenario sentences must be written using a controlled natural language (CNL) described according our use case transaction definition, which is based on Ochodek's transaction model [5]. We consider that a transaction is a sequence of four steps actions in a scenario, which starts from the actors request (U) and finishes with the system response (SR). The system validation (SV) and system expletive (SE) actions must also occur within the starting and ending action. The actions help to find out the B components. So, from SV actions we extract the preconditions and from SE actions we derive the operations names and the postconditions. We are not interested in the automatic translation of use cases for formal specifications since there are many natural language ambiguity problems. The intention of our work is to take the use cases as a guideline for starting B specifications. Our main goal is to create a new and complete development process (including deliverables artifacts), namely Be Velopment, for B focusing on agility/usability and we believe that use cases seem to be a good start point. © 2010 Springer.