Communications of the ACM
Automated Support For Diagnosis and Repair
Credit: HealthLens
Edward Feigenbaum and Raj Reddy won the ACM A.M. Turing Award in 1994 for their pioneering work demonstrating the practical importance and potential impact of artificial intelligence technology. Feigenbaum was influential in suggesting the use of rules and induction as a means for computers to learn theories from examples. In 2007, Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis won the Turing Award for developing model checking into a highly effective verification technology for discovering faults. Used in concert, verification and AI techniques can provide a powerful discovery and learning combination. In particular, the combination of model checking10 and logic-based learning15 has enormous synergistic potential for supporting the verify-diagnose-repair cycle software engineers commonly use in complex systems development. In this article, we show how to realize this synergistic potential.
Model checking exhaustively searches for property violations in formal descriptions (such as code, requirements, and design specifications, as well as network and infrastructure configurations), producing counterexamples when these properties do not hold. However, though model checkers are effective at uncovering faults in formal descriptions, they provide only limited support for understanding the causes of uncovered problems, let alone how to fix them. When uncovering a violation, model checkers usually provide one or more examples of how such a fault occurs in the description or model being analyzed. From this feedback, producing an explanation for the failure and generating a fix are complex tasks that tend to be human-intensive and error-prone. On the other hand, logic-based learning algorithms use correct examples and violation counterexamples to extend and modify a formal description such that the description conforms to the examples while avoiding the counterexamples. Although counterexamples are usually provided manually, examples and counterexamples can be provided through verification technology (such as model checking).
No entries found