Model Repair

Model Repair is an extended version of the Model Checking problem focusing on the automated quest of appropriate updates in a system's model, for the correction of qualitative or quantitative properties. In Model Checking, given a model M and a temporal logic formula φ, the problem is to determine if M satisfies φ. In the case of a negative result, a counterexample is returned in the form of an execution path in M leading to the violation of φ.

In Model Repair, given a model M and a temporal logic formula φ such that M does not satisfy φ, the problem is to obtain a new model M' such that M' satisfies φ, while the changes made to M to derive M' should be "minimal" with respect to all such M'. Model Repair has many applications in protocol design and elsewhere.

Abstract Model Repair [CBS12]

In [BGK11], we introduced the problem of Model Repair for quantitative properties of probabilistic systems. We showed how the problem can be reduced to a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique.

In [CBS12], we introduced an abstraction-refinement framework for the repair of Computation Tree Logic (CTL) formulas over Kripke Structures. Our approach aims to tackle the problem of the state space explosion, thus making possible to repair models with large or even infinite systems and to speed-up the repair process through the use of smaller abstract models.

Both works address the following fundamental questions regarding Model Repair:

  • What changes can be made to model M?
  • Is the repair of M feasible?
  • Is the Model Repair algorithm sound and complete?
  • How should be quantified the changes made to M?

Model Repair has been successfully applied to the design of DNS attack countermeasures ([BGK11], [ADB10], [DKB11]) and to a Kripke Structure model of the Andrew File System.

Contact persons: Prof. Panagiotis Katsaros, George Chatzieleftheriou
Joint work with: Prof. Scott Smolka, Prof. Radu Grosu, Prof. C.R. Ramakrishnan, Prof. Ezio Bartocci, Prof. Borzoo Bonakdarpour

Invited talk by Prof. P. Katsaros (Oxford University, 18-11-2013): Model Repair - Theory and Applications in Protocol Design     

Home | Projects | Publications | Partners | Related Links | News | People | Contact copyright � 2012 DSG group