Analysing Inconsistent Specifications

Anthony Hunter and Bashar Nuseibeh

Abstract

In previous work we advocated continued development of specifications in the presence of inconsistency. To support this we presented quasi-classical (QC) logic for reasoning with inconsistent specifications. The logic allows the derivation of non-trivial classical inferences from inconsistent information. In this paper we present a development called labelled QC logic, and some associated analysis tools, that allows the tracking and diagnosis of inconsistent information. The results of analysis are then used to guide further development in the presence of inconsistency. We illustrate the logic and our tools by specifying and analysing parts of the London Ambulance Service. We argue that the scalability of our approach is made possible by deploying the ViewPoints framework for multi-perspective development, such that our analysis tools are only used on partial specifications of a manageable size.

This paper is Proceedings of 3rd International Symposium on Requirements Engineering, 78-86, Annapolis, MD, USA, 5-10th January 1997.

It is also available over the Web: [compressed postscript version].






This research was sponsored by the EPSRC, under a research project entitled Managing Inconsistency in Software Engineering.