Abstract:
In computer science, formal verification techniques can assist programmers in designing highly reliable and stable software. Different from traditional testing, which can only find existing bugs by observing a subset of program behaviours, formal verification can use rigorous mathematical reasoning to cover all program behaviours. In formal verification-based software engineering, specifications of software can be represented using design models with a set of required properties. The consistency and completeness of design models can be formally verified using rigorous logical reasoning techniques, so that potential faults can be detected at an abstract level. However, repairing faulty design models is usually a manual process, which requires considerable human effort and reduces the efficiency of software development. To solve this problem, in this thesis, we study automated design model repair techniques based on formal verification and a number of extra repair techniques. Our techniques derive from the B-method, model checking, constraint solving, machine learning and automatic programming. We use the B-method to specify design models as abstract machines. Faults in the abstract machines are detected using model checking techniques. To eliminate detected faults, we suggest three general-purpose repair operators, i.e., modification, deletion and insertion, for repairing state spaces of abstract machines. The repair operators can generate candidate repairs using constraint solving techniques. Moreover, machine learning techniques are used to select highquality repairs. Machine learners can acquire semantic features of abstract machines from their state spaces and then select repairs by comparing the repairs with acquired semantic features. Further, selected repairs may be refactored into simpler forms using automatic programming techniques. We have implemented the automated model repair techniques as the B-repair tool. B-repair can repair invariant satisfiability and goal reachability of abstract machines, which are two of the most important properties in the B-method. We have demonstrated the effectiveness of B-repair on a number of public datasets of abstract machines. Moreover, we have studied how B-repair impacts the quality of abstract machines using the ISO/IEC 25010 international standard of software quality. Our study indicates that automated B model repair is feasible and effective and can improve formal verification-based software development.