Tools Overview Contact Us Publications Case Studies Manual Home


[BartocciGKRS11] Bartocci, E.; Grosu, R.; Katsaros, P.; Ramakrishnan, C. R. and Smolka, S. A. Model Repair for Probabilistic Systems. In TACAS, 2011.
Downloads: bibURL: Abstract. We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system M and a probabilistic temporal logic formula Phi such that M fails to satisfy Phi, the Model Repair problem is to find an M that satisfies Phi 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 significant 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.

Valid XHTML 1.1 Valid CSS! Powered by PHP