creators_name: Jastram, Michael creators_name: Leuschel, Michael creators_name: Bendisposto, Jens creators_name: Russo Jr, Aryldo G creators_id: jastram@cs.uni-duesseldorf.de creators_id: leuschel@cs.uni-duesseldorf.de creators_id: bendisposto@cs.uni-duesseldorf.de creators_id: agrj@aes.com.br type: other datestamp: 2009-05-26 08:39:21 lastmod: 2010-04-19 15:05:54 metadata_visibility: show title: Mapping Requirements to B models ispublished: unpub subjects: deploy_method_reqevo full_text_status: public pres_type: paper 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. Our objective is to find a practical way to establish traceability between natural language requirements and B models. We 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. In 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. refereed: FALSE citation: Jastram, Michael and Leuschel, Michael and Bendisposto, Jens and Russo Jr, Aryldo G Mapping Requirements to B models. UNSPECIFIED. (Unpublished) document_url: http://deploy-eprints.ecs.soton.ac.uk/104/1/2009-05_Requirements_Traceability.pdf