CaRE: a refinement calculus for requirements engineering based on argumentation theory

The Requirements Engineering (RE) process starts with initial requirements elicited from stakeholders—however conflicting, unattainable, incomplete and ambiguous—and successively refines them until a consistent, complete, valid, and unambiguous specification is reached. This is achieved by balancing stakeholders’ viewpoints and preferences to reach compromises through negotiation. Several frameworks have been developed to support this process in a structured way, such as KAOS, i*, and RationalGLR. However, none provides the means to model the dialectic negotiation inherent to the RE process, so that the derivation of specifications from requirements is fully explicit and traceable. To address this gap, we propose CaRE, a refinement calculus for requirements engineering based on argumentation theory. CaRE casts the RE refinement problem as an iterative argument between all relevant stakeholders, who point out defects (ambiguity, incompleteness, etc.) of existing requirements, and then propose suitable refinements to address them, thereby leading to the construction of a refinement graph. This graph is then a conceptual model of the RE process. The semantics of refinement graphs is provided using Argumentation Theory, enabling reasoning over the RE process and the automatic computation of software specifications. An alternate semantics is also presented based on abduction and using Horn Theory. The application of CaRE is showcased with an extensive example from the railway domain, and a prototype tool for identifying specifications in a refinement graph is presented.