We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system M and a probabilistic temporal logic formula f such that M fails to satisfy f, the Model Repair problem is to find an M' that satisfies f and differs from M only in the transition flows of those states in M that are deemed controllable. Moreover, the cost associated with modifying M's transition flows to obtain M' should be minimized. We show how the Model Repair problem can be formulated as an extended version of parametric probabilistic model checking, which translates into a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique. We demonstrate the practical utility of our approach by applying it to a number of signicant case studies, including a DTMC reward model of the Zeroconf protocol for assigning IP addresses, and a CTMC model of the highly publicized Kaminsky DNS cache-poisoning attack.
In Proc. of TACAS'11, the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Saarbruecken, Germany, March, 2011. Springer LNCS.
*This work was supported by the NSF Faculty Early Career
Development Award CCR01-33583, the NSF Expeditions Award
CNS-09-26190 and the NSF CCF05-23863 Award and the AFOSR
FA-0550-09-1-0481 Award.