Industrial deployment of system engineering methods providing high dependability and productivity


Starting B Specifications from Use Cases

Russo Jr, Aryldo G and de Sousa, Thiago (2010) Starting B Specifications from Use Cases. [DEPLOY Associate Item] (Unpublished)

PDF - Accepted Version


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.

Item Type:DEPLOY Associate Item
Subjects:Methodology > Requirements and evolution
ID Code:211
Deposited By:Mr Aryldo G Russo Jr
Deposited On:19 Mar 2010 10:47
Last Modified:19 Apr 2010 16:06

Repository Staff Only: item control page

Deploy-Project - All right reserved