Managing inconsistent specifications: reasoning, analysis and action

Abstract

In previous work, we have advocated continued development of speci-fications in the presence of inconsistency. To support this, we have used classical logic to represent partial specifications and to identify inconsis- tencies between them. We now present an adaptation of classical logic, which we term quasi-classic al (QC) logic, that allows continued reason- ing in the presence of inconsistency. The adaptation is a weakening of classical logic that prohibits all trivial derivations, but still allows all re- solvants of the assumptions to b e derived. Furthermore, the connectives behave in a classical manner. We then present a development called labelled QC logic that records and tracks assumptions used in reasoning. This facilitates a logical analysis of inconsistent information. We discuss the application of lab elled QC logic in the analysis of multi-perspective specifications. Such specifications are developed by multiple participants who hold overlapping, often inconsistent, views of the systems they are developing. Finally, we discuss further the notion of acting in the presence of inconsistency, and examine the use of meta-level inconsistency handling rules to support such action. The feasibility of automated support for this kind of inconsistency handling is also discussed, and related work in the area is critically reviewed.