Starting B Specifications from Use Cases

The B method is one of the most used formal methods, when reactive systems is under question, due to good support for refinement. However, obtaining the formal model from requirements is still an open issue, difficult to be tackle in any notation due the background distance between the requirement engineer and the one in charge of work with a formal specification. On the other hand, use cases have become the informal industry standard for capturing how the end user interacts with the software by detailing scenario-driven threads. Furthermore, the scenarios steps provide an easy way to derive functional tests, as in the same way what has to be achieved and what's not is, normally, clearly stated. In this paper we show how controlled use cases and functional tests based on them can be used as a guideline for writing B operations and invariants. As a side effect, we also present a practical way to establish traceability between functional requirements and formal models. Keywords. B m...

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Thiago C. de Sousa, Aryldo G. Russo
• Keywords: ASM 2010, Computational Biology, Formal Methods, Formal Models, Functional Tests