Industrial deployment of system engineering methods providing high dependability and productivity


Mapping Requirements to B models

Jastram, Michael and Leuschel, Michael and Bendisposto, Jens and Russo Jr, Aryldo G Mapping Requirements to B models. UNSPECIFIED. (Unpublished)



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.

Item Type:Other
Subjects:Methodology > Requirements and evolution
ID Code:104
Deposited By:Michael Jastram
Deposited On:26 May 2009 09:39
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved