Industrial deployment of system engineering methods providing high dependability and productivity


An Approach of Requirements Tracing in Formal Refinement

Jastram, Michael and Hallerstede, Stefan and Leuschel, Michael and Russo Jr, Aryldo G (2010) An Approach of Requirements Tracing in Formal Refinement. In: VSTTE’10 Verified Software: Theories, Tools and Experiments, 16th-19th August 2010, Edinburgh, UK. (In Press)

This is the latest version of this item.

PDF - Accepted Version


Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements. We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.

Item Type:Conference or Workshop Item (Paper)
Uncontrolled Keywords:Requirements Traceability, WRSPM, Formal Modeling, Refinement, Event-B
Subjects:Methodology > Requirements and evolution
Training > Rodin plug-ins
ID Code:236
Deposited By:Mr Michael Jastram
Deposited On:08 Jul 2010 10:48
Last Modified:18 Jul 2010 23:51

Available Versions of this Item

Repository Staff Only: item control page

Deploy-Project - All right reserved