Using Abduction to Evolve Inconsistent Requirements Specification

Requirements specifications are often inconsistent. Inconsistencies may arise because multiple conflicting requirements are embodied in these specifications, or because the specifications themselves are in a transient stage of evolutionary development. In this paper we argue that such inconsistencies, rather than being undesirable, are actually useful drivers for changing the requirements specifications in which they arise. We present a formal technique to reason about inconsistency handling changes. Our technique is an adaptation of logical abduction - adapted to generate changes that address some specification inconsistencies, while leaving others. We represent our specifications in quasi-classical (QC) logic - an adaptation of classical logic that allows continued reasoning in the presence of inconsistency. The paper develops a sound algorithm for automating our abductive reasoning technique and presents illustrative examples drawn from a library system case study