--- abstract: "Formal methods in systems engineering are gaining traction, at least in some areas. While the formal specification process from abstraction via refinement to implementation is fairly well understood, the traceability between the initial user requirements and the formal model is still unsatisfying. There are some promising attempts (e.g. KAOS) that inspired some of the work done here.\r\n\r\nOur objective is to find a practical way to establish traceability between natural language requirements and B models.\r\n\r\nWe select a number of existing methods and notations for bringing natural language requirements and B specifications together. Specifically, we use UML-B for building a data model; we use invariants (part of the B method) to model safety requirements; and we use temporal expressions (LTL) to model liveness requirements.\r\n\r\nIn this paper, we show a pragmatic way that may lead to a method for making traceability between natural language requirements and B models easier to understand, maintain and validate." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - jastram@cs.uni-duesseldorf.de - leuschel@cs.uni-duesseldorf.de - bendisposto@cs.uni-duesseldorf.de - agrj@aes.com.br creators_name: - family: Jastram given: Michael honourific: '' lineage: '' - family: Leuschel given: Michael honourific: '' lineage: '' - family: Bendisposto given: Jens honourific: '' lineage: '' - family: Russo Jr given: Aryldo G honourific: '' lineage: '' data_type: ~ date: ~ date_type: ~ datestamp: 2009-05-26 08:39:21 department: ~ dir: disk0/00/00/01/04 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 104 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/104/1/2009%2D05_Requirements_Traceability.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:05:54 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: ~ publisher: ~ refereed: FALSE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 18 series: ~ skill_areas: [] source: ~ status_changed: 2009-05-26 08:39:21 subjects: - deploy_method_reqevo succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Mapping Requirements to B models type: other userid: 10 volume: ~