Traceability - lgwagner/SpeAR GitHub Wiki

Traceability is a feature of the Logical Entailment analysis that is useful for understanding which requirements were necessary to prove each property. Traceability analysis identifies which requirements were necessary to prove each property. When the Preferences IVC option is enabled, SpeAR will automatically provide a traceability matrix option for each proven property. In addition, it will emit an additional property that is the conjunct of all the properties in the specification. The traceability matrix for this property will identify all of the requirements that are necessary to prove all the properties in a given file.

This example shows a simple specification with three inputs, and three outputs. By inspection one can tell that r0 is needed to prove p0, r1 is needed to prove p1, and r2 is needed to prove p2. The associated traceability matrix provides this information, plus it provides an additional property called all_properties, which is useful when determining which requirements are necessary to prove all the properties in a specification.

If the Properties section of a specification is representative of a high-level requirement, and the Requirements section is representative of a low-level requirement, SpeAR can be used to establish traceability in both directions. First, if a given property is proven against a set of requirements, this demonstrates that the requirements (the low-level requirements) satisfy the property (a high-level requirement), and thus each property traces to a set of requirements. The Traceability analysis can then be used to show that each requirement (the low-level requirement) traces to a given property. This analysis can be useful for identifying unused or unnecessary requirements.