A Method and Tool for Tracing Requirements into Specifications
[PDF] [Bibtex]Submitted to Science of Computer Programming
The creation of a consistent system description is a challenging problem of requirements engineering. Formal and informal reasoning can greatly contribute to meet this challenge. However, this demands that formal and informal reasoning and the system description are connected in such way that the reasoning permits drawing conclusions about the system description.
We describe an incremental approach to requirements modelling and validation that incorporates formal and informal reasoning. Our main contribution is an approach to requirements tracing that delivers the necessary connection that links the reasoning to the system description. Formal refinement is used in order to deal with large and complex system descriptions.
We discuss tool support for our approach of requirements tracing that combines informal requirements modelling with formal modelling and verification while tracing requirements among each other and into the formal model.
Requirements Traceability between Textual Requirements and Formal Models Using ProR
[PDF] [Bibtex]Accepted for iFM'2012
Traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. Previously, we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W /\ S => R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts.
We created tool support for this approach by integrating Rodin and ProR ...
Mixing Formal and Informal Model Elements for Tracing Requirements
[PDF] [Bibtex]In booktitle, AVOCS 2011, 2011.
Tracing between informal requirements and formal models is challenging. A method for such tracing should permit to deal efficiently with changes to both the requirements and the model. A particular challenge is posed by the persisting interplay of formal and informal elements.
In this paper, we describe an incremental approach to requirements validation and systems modelling. Formal modelling facilitates a high degree of automation: it serves for validation and traceability.
The foundation for our approach are requirements that are structured according to the WRSPM reference model. We provide a system for traceability with a state-based formal method that supports refinement. We do not require all specification elements to be modelled formally and support incremental incorporation of new specification elements into the formal model. Refinement is used to deal with larger amounts of requirements in a structured way.
We provide a small example using Problem Frames and Event-B to demonstrate our approach.
In Proceedings of FMICS 2009, volume 5825 of Lecture Notes in Computer Science, Springer, 2009.
B-MotionStudio provides a way to quickly generate domain specific visualisations for a formal model, enabling domain experts and managers to understand and validate the model. We also believe that our tool will be of use when teaching formal methods, both during lectures as a way to motivate students to write their own formal models.
