Model repair for probabilistic systems. (English) Zbl 1316.68070
Abdulla, Parosh Aziz (ed.) et al., Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 326-340 (2011).
Summary: We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system \(M\) and a probabilistic temporal logic formula \(\varphi \) such that \(M\) fails to satisfy \(\varphi \), the Model Repair problem is to find an \(M^{\prime}\) that satisfies \(\varphi \) 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^{\prime}\) should be minimized. Using a new version of parametric probabilistic model checking, we show how the Model Repair problem can be reduced to 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.
For the entire collection see [Zbl 1213.68016].
For the entire collection see [Zbl 1213.68016].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 90C30 | Nonlinear programming |
References:
| [1] | Alexiou, N., Deshpande, T., Basagiannis, S., Smolka, S.A., Katsaros, P.: Formal analysis of the kaminsky DNS cache-poisoning attack using probabilistic model checking. In: Proceedings of the 12th IEEE International High Assurance Systems Engineering Symposium, pp. 94–103. IEEE Computer Society, Los Alamitos (2010) |
| [2] | Biegler, L.T., Zavala, V.M.: Large-scale nonlinear programming using IPOPT: An integrating framework for enterprise-wide dynamic optimization. Computers & Chemical Engineering 33(3), 575–582 (2009) · doi:10.1016/j.compchemeng.2008.08.006 |
| [3] | Bonakdarpour, B., Ebnenasir, A., Kulkarni, S.S.: Complexity results in revising UNITY programs. ACM Trans. Auton. Adapt. Syst. 4(1), 1–28 (2009) · doi:10.1145/1462187.1462192 |
| [4] | Boyd, S., Vandenberghe, L.: Convex Optimization. Camb. Univ. Press, Cambridge (2004) · doi:10.1017/CBO9780511804441 |
| [5] | Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artif. Intell. 112(1-2), 57–104 (1999) · Zbl 0996.68104 · doi:10.1016/S0004-3702(99)00039-9 |
| [6] | Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: Algorithmic verification and debugging. Communications of the ACM 52(11), 74–84 (2009) · doi:10.1145/1592761.1592781 |
| [7] | Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005) · Zbl 1108.68497 · doi:10.1007/978-3-540-31862-0_21 |
| [8] | Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-88562-7_20 |
| [9] | Dong, Y., Sarna-Starosta, B., Ramakrishnan, C.R., Smolka, S.A.: Vacuity checking in the modal mu-calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 147–162. Springer, Heidelberg (2002) · Zbl 1275.68090 · doi:10.1007/3-540-45719-4_11 |
| [10] | Epifani, I., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Model evolution by run-time parameter adaptation. In: ICSE 2009: Proceedings of the 31st International Conference on Software Engineering, pp. 111–121. IEEE Computer Society Press, Washington, DC, USA (2009) · doi:10.1109/ICSE.2009.5070513 |
| [11] | Giacalone, A., Chang Jou, C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proc. of the IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 443–458. North-Holland, Amsterdam (1990) |
| [12] | Granvilliers, L., Benhamou, F.: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32, 138–156 (2006) · Zbl 1346.65020 · doi:10.1145/1132973.1132980 |
| [13] | Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer, 1–17 (April 2010) |
| [14] | Hahn, E.M.: Parametric Markov model analysis. Master’s thesis, Saarland University (2008) |
| [15] | Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: A Model Checker for Parametric Markov Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660–664. Springer, Heidelberg (2010) · doi:10.1007/978-3-642-14295-6_56 |
| [16] | Han, T., Katoen, J.-P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: IEEE International Real-Time Systems Symposium, pp. 173–182 (2008) · doi:10.1109/RTSS.2008.19 |
| [17] | Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 102–111 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [18] | Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226–238. Springer, Heidelberg (2005) · Zbl 1081.68572 · doi:10.1007/11513988_23 |
| [19] | Knuth, D., Yao, A.: The complexity of nonuniform random number generation. In: Algorithms and Complexity: New Directions and Recent Results. Academic Press, London (1976) |
| [20] | Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007) · Zbl 1323.68379 · doi:10.1007/978-3-540-72522-0_6 |
| [21] | Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system sesign and analysis. Formal Aspects of Computing 19(1), 93–109 (2007) · Zbl 1111.68084 · doi:10.1007/s00165-006-0015-2 |
| [22] | Sinha, S.M.: Duality in nonlinear programming. In: Mathematical Programming, pp. 423–430. Elsevier Science, Burlington (2006) · doi:10.1016/B978-813120376-7/50027-0 |
| [23] | Zhang, D., Cleaveland, R.: Fast on-the-fly parametric real-time model checking. In: Proceedings of the 26th IEEE International Real-Time Systems Symposium, pp. 157–166. IEEE Computer Society, Los Alamitos (2005) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
