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.
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.
