Managing inconsistent specifications: reasoning, analysis, and action

ABSTRACT

In previous work, we advocated continued development of specifications in the presence of inconsistency. To support this, we used classical logic to represent partial specifications and to identify inconsistencies between them. We now present an adaptation of classical logic, which we term quasi-classical (QC) logic, that allows continued reasoning in the presence of inconsistency. The adaptation is a weakening of classical logic that prohibits all trivial derivations, but still allows all resolvants of the assumptions to be derived. Furthermore, the connectives behave in a classical manner. We then present a development called labeled QC logic that records and tracks assumptions used in reasoning. This facilitates a logical analysis of inconsistent information. We discuss that application of labeled QC logic in the analysis of multiperspective specifications. Such specifications are developed by multiple particpants who hold overlapping, often inconsistent, views of the systems they are developing.

REFERENCES

• 1: Will Atkinson , Jim Cunningham, Proving properties of a safety-critical system, Software Engineering Journal, v.6 n.2, p.41-50, March 1991
• 2: Robert Balzer, Tolerating inconsistency, Proceedings of the 13th international conference on Software engineering, p.158-165, May 13-17, 1991, Austin, Texas, United States
• 3: BARAL, C., KRAUS, S., MINKER, J., AND SUBRAHMANIAN, V. 1992. Combining knowledge bases consisting of first order theories. Computational Intelligence 8, 45-71.
• 4: BEARNE, M. 1996. Hypermedia visualization for system requirements in a collaborative distributive environment. Technical Report TN3491, Philips Research Labs, Redhill, Surrey.
• 5: BELNAP, N. 1977. A useful four-valued logic. In G. Epstein Ed., Modern Uses of Multiple- Valued Logic (1977), pp. 8-37. Reidel.
• 6: BENFERHAT, S., DUBOIS, D., AND PRADE, g. 1993. Argumentative inference in uncertain and inconsistent knowledge bases. In Proceedings of Uncertainty in Artificial Intelligence (1993). Morgan Kaufmann.
• 7: BESNARD, P. 1991. Paraconsistent logic approach to knowledge representation. In M. de Glas M and D. G. D. Eds., Proceedings of the First World Conference on Fundamentals of Artificial Intelligence (1991), pp. 107-114. Angkor.
• 8: Philippe Besnard , Anthony Hunter, Quasi-classical Logic: Non-trivializable classical reasoning from incosistent information, Proceedings of the European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, p.44-51, July 03-05, 1995
• 9: BIBEL, W. 1993. Deduction: Automated logic. Academic Press.
• 10: Alexander Borgida, Language features for flexible handling of exceptions in information systems, ACM Transactions on Database Systems (TODS), v.10 n.4, p.565-603, Dec. 1985 [doi>10.1145/4879.4995]
• 11: Christophe Bourely , Ricardo Caferra , Nicolas Peltier, A Method for Building Models Automatically. Experiments with an Extension of OTTER, Proceedings of the 12th International Conference on Automated Deduction, p.72-86, June 26-July 01, 1994
• 12: BREWKA, G. 1989. Preferred subtheories: An extended logical framework for default reasoning. In Proceedings of the Eleventh International Conference on Artificial Intelligence (1989), pp. 1043-1048.
• 13: Ricardo Caferra , Nicolas Pelier, Model Building and Interactive Theory Discovery, Proceedings of the 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, p.154-168, May 07-10, 1995
• 14: CAFERRA, R. AND ZABEL, N. 1993. Building models by using tableaux extended by equational problems. Journal of Logic and Computation 8, 3-25.
• 15: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 16: M. C. Costa , R. J. Cunningham , J. Booth, Logical animation, Proceedings of the 12th international conference on Software engineering, p.144-149, March 26-30, 1990, Nice, France
• 17: Gianpaolo Cugola , Elisabetta Di Nitto , Alfonso Fuggetta , Carlo Ghezzi, A framework for formalizing inconsistencies and deviations in human-centered systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.191-230, July 1996 [doi>10.1145/234426.234427]
• 18: G. Cugola , E. Di Nitto , C. Ghezzi , M. Mantione, How to deal with deviations during process model enactment, Proceedings of the 17th international conference on Software engineering, p.265-273, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225039]
• 19: DA COSTA, N.C. 1974. On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic 15, 497-510.
• 20: DOWSON, M. 1993. Consistency maintenance in process sensitive environments. In Proceedings of Workshop on Process Sensitive Environments Architectures (Boulder, Colorado, USA, 1993). Rocky Mountain Institute of Software Engineering (RMISE).
• 21: DOYLE, J. 1979. A truth maintenance system. Artificial Intelligence 12, 231-272.
• 22: S. Easterbrook , B. Nuseibeh, Managing inconsistencies in an evolving specification, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.48, March 27-29, 1995
• 23: EASTERBROOK, S. AND NUSEIBEH, B. 1996. Using viewpoints for inconsistency management. BCS/IEE Software Engineering Journal 11, 1, 31-43.
• 24: Morten Elvang-Gøransson , Anthony Hunter, Argumentative logics: reasoning with classically inconsistent information, Data & Knowledge Engineering, v.16 n.2, p.125-145, Aug. 1995 [doi>10.1016/0169-023X(95)00013-I ]
• 25: Martin S. Feather, Modularized exception handling, Joint proceedings of the second international software architecture workshop (ISAW-2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops, p.167-171, October 16-18, 1996, San Francisco, California, United States [doi>10.1145/243327.243644]
• 26: A. Finkelstein , J. Dowell, A comedy of errors: the London Ambulance Service case study, Proceedings of the 8th International Workshop on Software Specification and Design, p.2, March 22-23, 1996
• 27: A. C. W. Finkelstein , D. Gabbay , A. Hunter , J. Kramer , B. Nuseibeh, Inconsistency Handling in Multiperspective Specifications, IEEE Transactions on Software Engineering, v.20 n.8, p.569-578, August 1994 [doi>10.1109/32.310667 ]
• 28: FINKELSTEIN, A., KRAMER, J., NUSEIBEH, B., FINKELSTEIN, L., AND GOEDICKE, M. 1992. Viewpoints: A framework for multiple perspectives in system development. International Journal of Software Engineering and Knowledge Engineering (Special issue on Trends and Future Research Directions in Software Engineering Environments) 2, 1, 31-57.
• 29: Melvin Fitting , David Gries, First-order logic and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1990
• 30: Dov M. Gabbay , Anthony Hunter, Making inconsistency respectable: a logical framework for inconsistency in reasoning, Proceedings of the International Workshop on Fundamentals of Artificial Intelligence Research, p.19-32, September 08-13, 1991
• 31: Dov M. Gabbay , Anthony Hunter, Making Inconsistency Respectable: Part 2 - Meta-level handling of inconsistency, Proceedings of the European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, p.129-136, November 08-10, 1993
• 32: GABBAY, D. AND HUNTER, A. 1998. Negation and contradiction. In What is negation? Kluwer.
• 33: Torben Mejlvang Hangensen , Bent Bruun Kristensen, Consistency in software system development: framework, model, techniques & tools, ACM SIGSOFT Software Engineering Notes, v.17 n.5, p.58-67, Dec. 1992
• 34: HUNTER, A. 1996. Reasoning with contradictory information using quasi-classical logic. In Technical report (1996). Department of Computer Science, University College London. Available from www.cs.ucl.ac.uk/staff/a.hunter.
• 35: Anthony Hunter, Paraconsistent logics, Handbook of defeasible reasoning and uncertainty management systems: volume 2: reasoning with actual and potential contradictions, Kluwer Academic Publishers, Norwell, MA, 1998
• 36: Anthony Hunter , Bashar Nuseibeh, Analyzing Inconsistent Specifications, Proceedings of the 3rd IEEE International Symposium on Requirements Engineering (RE'97), p.78, January 05-08, 1997
• 37: Johan de Kleer, An assumption-based TMS, Artificial Intelligence, v.28 n.2, p.127-162, March 1986 [doi>10.1016/0004-3702(86)90080-9 ]
• 38: Paul Krause , Dominic Clark, Representing Uncertain Knowledge: An Artificial Intelligence Approach, Kluwer Academic Publishers, Norwell, MA, 1993
• 39: Larry Wos , Ross Overbeek , Ewing Lusk , Jim Boyle, Automated reasoning (2nd ed.): introduction and applications, McGraw-Hill, Inc., New York, NY, 1992
• 40: Ulf Leonhardt , Jeff Kramer , Bashar Nuseibeh, Decentralised process enactment in a multi-perspective development environment, Proceedings of the 17th international conference on Software engineering, p.255-264, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225038]
• 41: LINDSAY, P. A. 1988. A survey of mechanical support for formal reasoning. BCS/IEE Software Engineering Journal (special issue on mechanical support for formal reasoning) 3, 1.
• 42: MCCUNE, W. 1990. OTTER 2.0 user's guide. Technical Report ANL-90/9, Argonne National Laboratory, Argonne, Illinois.
• 43: K. Narayanaswamy , Neil Goldman, “Lazy” consistency: a basis for cooperative software development, Proceedings of the 1992 ACM conference on Computer-supported cooperative work, p.257-264, November 01-04, 1992, Toronto, Ontario, Canada [doi>10.1145/143457.143521]
• 44: Bashar Nuseibeh, To Be and Not to Be: On Managing Inconsistency in Software Development, Proceedings of the 8th International Workshop on Software Specification and Design, p.164, March 22-23, 1996
• 45: NUSEIBEH, B. AND FINKELSTEIN, A. 1992. Viewpoints: A vehicle for method and tool integration. In Proceedings of 5th International Workshop on Computer-Aided Software Engineering (CASE '92) (Montreal, Canada, 1992), pp. 50-60. IEEE Computer Society Press.
• 46: Bashar Nuseibeh , Jeff Kramer , Anthony Finkelstein, A Framework for Expressing the Relationships Between Multiple Views in Requirements Specification, IEEE Transactions on Software Engineering, v.20 n.10, p.760-773, October 1994 [doi>10.1109/32.328995 ]
• 47: Bashar Nuseibeh , Alessandra Russo, On the Consequences of Acting in the Presence of Inconsistency, Proceedings of the 9th international workshop on Software specification and design, p.156, April 16-18, 1998
• 48: David Poole, A logical framework for default reasoning, Artificial Intelligence, v.36 n.1, p.27-47, August 1988 [doi>10.1016/0004-3702(88)90077-X ]
• 49: PRAKKEN, H. 1993. An argument framework for default reasoning. In Annals of mathematics and artificial intelligence, Volume 9 (1993).
• 50: Alessandra Russo , Bashar Nuseibeh , Jeff Kramer, Restructuring Requirements Specifications For Managing Inconsistency And Change: A Case Study, Proceedings of the 3rd International Conference on Requirements Engineering: Putting Requirements Engineering to Practice, p.51, April 06-10, 1998
• 51: RYAN, M. 1992. Representing defaults as sentences with reduced priority. In Principles of Knowledge Representation and Reasoning: Proceedings of the Third International Conference (1992). Morgan Kaufmann.
• 52: SCHUMANN, J. 1993. SCOTT: A model-guided theorem prover. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI '93) (1993), pp. 109-114.
• 53: SCHUMANN, J. 1994. SETHEO V3.2: Recent developments. In Proceedings of the Twelfth Conference on Computer-Aided Deduction (CADE-12), Volume 814 of Lecture Notes in Computer Science (1994). Springer.
• 54: SCHWANKE, R. W. AND KAISER, G.E. 1988. Living with inconsistency in large systems. In Proceedings of the International Workshop on Software Version and Configuration Control (1988), pp. 98-118. B G Teubner.
• 55: SLANEY, J. 1996. FINDER: Finite domain enumerator version 3 notes and guide. Technical report, Centre for Information Science Research, Australian National University.
• 56: Pamela Zave , Michael Jackson, Conjunction as composition, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.4, p.379-411, Oct. 1993 [doi>10.1145/158431.158438]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)
      D.2.4 Software/Program Verification
          Subjects: Validation
      D.2.5 Testing and Debugging
          Subjects: Error handling and recovery
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Restructuring, reverse engineering, and reengineering

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Design, Languages, Theory, Verification

Keywords:
managing inconsistency, paraconsistent logics, requiriements specification, viewpoints