Starting B Specifications from Use Cases

11 years 9 months ago
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...
Thiago C. de Sousa, Aryldo G. Russo
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where ASM
Authors Thiago C. de Sousa, Aryldo G. Russo
Comments (0)