Enhancing model checking in verification by AI techniques

Model checking is a fruitful application of computational logic with high r elevance to the verification of concurrent systems. While model checking is capable of automatically testing that a concurrent system satisfies its fo rmal specification, it can not precisely locate an error and suggest a repa ir, i.e., a suitable correction, to the system. In this paper, we tackle th is problem by using principles from AI. In particular, we introduce the abs tract concept of a system repair problem, and exemplify this concept on rep air of concurrent programs and protocols. For the development of our framew ork, we formally extend the concept of counterexample, which has been propo sed in model checking previously, and provide examples which demonstrate th e need for such an extension. Moreover, we investigate into optimization is sues for the problem of finding a repair, and present techniques which gain in some cases a considerable reduction of the search space for a repair. ( C) 1999 Elsevier Science B.V. All rights reserved.