--- 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." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - agrj@aes.com.br - ~ creators_name: - family: Russo Jr given: Aryldo G honourific: '' lineage: '' - family: de Sousa given: Thiago honourific: '' lineage: '' data_type: ~ date: 2010 date_type: ~ datestamp: 2010-03-19 10:47:28 department: ~ dir: disk0/00/00/02/11 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 211 event_dates: ~ event_location: ~ event_title: ABZ 2010 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/211/1/paper_63%2D3.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: unpub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:06:00 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: 'Abstract State Machines (ASM), Alloy, B and Z Conference' publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 25 series: ~ skill_areas: [] source: ~ status_changed: 2010-03-19 10:47:28 subjects: - deploy_method_reqevo succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Starting B Specifications from Use Cases type: deploy_associate_item userid: 22 volume: 'to be '