A method and tool for tracing requirements into specifications

• We created an incremental approach for building a system description consisting of formal and informal artefacts.
• We created an approach to traceability that supports systematic validation and change management.
• The work described here is supported by a tool integrating requirements modelling, formal modelling and model checking.

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 a 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 to requirements tracing that combines informal requirements modelling with formal modelling and verification while tracing requirements among each other and into the formal model.