Model Repair: theory and applications in protocol design

Model Repair is the automated quest of appropriate updates in a model, for the correction of qualitative or quantitative system properties. We consider the cases of Model Repair for Kripke structures and Model Repair for probabilistic systems. Given a model M and a (probabilistic) CTL formula φ where M does not satisfy φ, the problem of Model Repair 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’. We consider a solution to the Model Repair of probabilistic systems via a reduction to a nonlinear optimization problem with a minimal-cost objective function. For Kripke structures, we present a framework for Model Repair that uses abstraction-refinement to tackle the problem of state space explosion. We discuss applications of Model Repair in protocol design: (i) the security hardening of the DNS (Domain Name System) and (ii) the repair of a model of the Andrew File System protocol. Finally, we comment on other recent solution proposals. The talk is based on two research papers:

1. Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, CR, Smolka, S. Model Repair for probabilistic systems, In Proceedings of the 17th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Saarbrucken, Germany, LNCS 6605, 326-340, Springer Verlag, 2011

2. Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S., Katsaros, P. Abstract model repair, In Proceedings of the 4th NASA Formal Methods Symposium (NFM), Norfolk, Virginia, LNCS 7226, 341-355, Springer Verlag, 2012