Combining abductive reasoning and inductive learning to evolve requirements specifications

Abstract

The development of requirements specifications inevitably involves modification and evolution. To support modification while preserving the main requirements goals and properties, we propose the use of a cycle composed of two phases: analysis and revision. In the analysis phase, a desirable property of the system is checked against a partial specification. Should the property be violated, diagnostic information is provided. In the revision phase, the diagnostic information is used to help modify the specification in such a way that the new specification no longer violates the original property. We have investigated a particular instance of such a cycle that combines the techniques of logical abduction and inductive learning to analyse and revise specifications respectively. Given an (event-based) system description and a system property, our abductive reasoning mechanism identifies a set of counter-examples of the property, if any exists. This set is then used to generate a corresponding set of examples of system behaviours that should be covered by the system description. These examples are used as training examples by our inductive learning mechanism, which performs the necessary changes to the system description in order to resolve the property violation. The approach is supported by an abductive decision procedure and a hybrid (neural and symbolic) learning system that we have developed. A case study of an automobile cruise control system illustrates our approach and provides some early validation of its capabilities.