Formal Semantics of Requirements Relationships for Traceability

Proving that a system satisfies its requirements is an important challenge of Requirements Engineering (RE). Requirements traceability is one of the answer given by RE to ensure that the system is the ``right'' system. Formal approaches provide a way to mathematically express requirements and to prove that a system satisfies its requirements. But most of the time the traceability is not formally defined, and neither are relationships between requirements. In this paper we have identified eight relationships between requirements. We provide their formal definitions and properties on the propagation of the satisfaction state. These definitions can help engineers not only to verify requirements (by checking the validity of the semantics of the relationships between two requirements), but also to verify the system compliance (thanks to satisfaction propagation). To validate these definitions, we implement them into a programming language, and we use a theorem prover to validate and verify examples of requirements formalized in this programming language. This work is a step towards the introduction of formal semantics into traceability, making possible to automatically analyze requirements and to use their relationships to verify the corresponding implementation of the system.