Abstract model repair

Abstract

Given a Kripke structure M and CTL formula φ, where M | ≠ φ, the problem of Model Repair is to obtain a new model M′ such that M′ |= φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our model-repair framework is based on Kripke Structures, a 3-valued semantics for CTL, and Kripke Modal Transition Systems (KMTSs), and features an abstract-model-repair algorithm for KMTSs. Application to an Automatic Door Opener system is used to illustrate the practical utility of abstract model repair. © 2012 Springer-Verlag.