creators_name: Russo Jr, Aryldo G creators_name: de Sousa, Thiago creators_id: agrj@aes.com.br type: deploy_associate_item datestamp: 2010-03-19 10:47:28 lastmod: 2010-04-19 15:06:00 metadata_visibility: show title: Starting B Specifications from Use Cases ispublished: unpub subjects: deploy_method_reqevo full_text_status: public pres_type: paper 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. date: 2010 publication: Abstract State Machines (ASM), Alloy, B and Z Conference volume: to be event_title: ABZ 2010 event_type: conference refereed: TRUE citation: Russo Jr, Aryldo G and de Sousa, Thiago (2010) Starting B Specifications from Use Cases. [DEPLOY Associate Item] (Unpublished) document_url: http://deploy-eprints.ecs.soton.ac.uk/211/1/paper_63-3.pdf