Combining abductive reasoning and inductive learning to evolve requirements specifications

The development of requirements specifications inevitably involves modification and evolution. To support modification while preserving particular requirements goals and properties, the use of a cycle composed of two phases: analysis and revision is proposed. 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. An instance of the above analysis-revision cycle that combines new techniques of logical abduction and inductive learning to analyse and revise specifications, respectively is investigated. More specifically, given an (event-based) system description and a system property, abductive reasoning is applied in refutation mode to verify whether the description satisfies the property and, if it does not, identify diagnostic information in the form of a set of examples of property violation. These (counter) examples are then used to generate a corresponding set of examples of system behaviours that should be covered by the system description. Finally, such examples are used as training examples for inductive learning, changing the system description in order to resolve the property violation. This is accomplished with the use of the connectionist inductive learning and logic programming system-a hybrid system based on neural networks and the backpropagation learning algorithm. A case study of an automobile cruise control system illustrates the approach and provides some early validation of its capabilities.