zbMATH — the first resource for mathematics

Counterexample-guided predicate abstraction of hybrid systems. (English) Zbl 1088.68096
Summary: Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counterexamples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counterexamples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.A.; Ho, P.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoret. comput. sci., 138, 3-34, (1995) · Zbl 0874.68206
[2] Alur, R.; Dang, T.; Esposito, J.; Hur, Y.; Ivančić, F.; Kumar, V.; Lee, I.; Mishra, P.; Pappas, G.; Sokolsky, O., Hierarchical modeling and analysis of embedded systems, Proc. IEEE, 91, 1, 11-28, (2003)
[3] Alur, R.; Dang, T.; Ivančić, F., Reachability analysis of hybrid systems via predicate abstraction, (), 35-48 · Zbl 1044.93517
[4] R. Alur, T. Dang, F. Ivančić, Reachability analysis of hybrid systems using counter-example guided predicate abstraction, Technical Report MS-CIS-02-34, University of Pennsylvania, Philadelphia, PA, November 2002.
[5] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[6] Alur, R.; Itai, A.; Kurshan, R.P.; Yannakakis, M., Timing verification by successive approximation, Inform. and comput., 118, 1, 142-157, (1995) · Zbl 0939.68705
[7] Asarin, E.; Bournez, O.; Dang, T.; Maler, O., Approximate reachability analysis of piecewise linear dynamical systems, (), 21-31 · Zbl 0938.93502
[8] Ball, T.; Rajamani, S., Bebop: a symbolic model checker for Boolean programs, (), 113-130 · Zbl 0976.68540
[9] Barber, C.; Dobkin, D.; Huhdanpaa, H., The quickhull algorithm for convex hulls, ACM trans. math. software, 22, 4, 469-483, (1996) · Zbl 0884.65145
[10] Cameron, S., A comparison of two fast algorithms for computing the distance between convex polyhedra, IEEE trans. robotics automation, 13, 6, 915-920, (1997)
[11] Chutinan, A.; Krogh, B.K., Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations, (), 76-90 · Zbl 0954.93020
[12] Clarke, E.; Fehnker, A.; Han, Z.; Krogh, B.; Stursberg, O.; Theobald, M., Verification of hybrid systems based on counterexample-guided abstraction refinement, (), 192-207 · Zbl 1031.68078
[13] Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (), 154-169 · Zbl 0974.68517
[14] Clarke, E.M.; Fehnker, A.; Han, Z.; Krogh, B.; Ouaknine, J.; Stursberg, O.; Theobald, M., Abstraction and counterexample-guided refinement of hybrid systems, Internat. J. found. comput. sci., 14, 3, (2003) · Zbl 1101.68678
[15] Clarke, E.M.; Kurshan, R.P., Computer-aided verification, IEEE spectrum, 33, 6, 61-67, (1996)
[16] Corbett, J.C.; Dwyer, M.B.; Hatcliff, J.; Laubach, S.; Pasareanu, C.S.; Robby; Zheng, H., Bandera: extracting finite-state models from Java source code, (), 439-448
[17] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (), 238-252
[18] Das, G.; Joseph, D., The complexity of minimum convex nested polyhedra, ()
[19] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool K{\scronos}, ()
[20] Dobkin, D.; Kirkpatrick, D., Determining the separation of preprocessed polyhedra—a unified approach, (), 400-413 · Zbl 0765.68205
[21] Edelsbrunner, H.; Preparata, F.P., Minimum polygon separation, Inform. and comput., 77, 218-232, (1987) · Zbl 0642.52004
[22] K. Fukuda, cddlib reference manual, cddlib version 092a, Technical Report, McGill University, 2001.
[23] Henzinger, T.A.; Ho, P.; Wong-Toi, H., H{\scy}T{\scech}: the next generation, (), 56-65
[24] Henzinger, T.A.; Ho, P.; Wong-Toi, H., H{\scy}T{\scech}: a model checker for hybrid systems, Software tools technol. transfer, 1, (1997)
[25] Henzinger, T.A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, (), 58-70 · Zbl 1323.68374
[26] Holzmann, G.J., The model checker SPIN, IEEE trans. software eng., 23, 5, 279-295, (1997)
[27] Holzmann, G.J.; Smith, M.H., Automating software feature verification, Bell labs technical J., 5, 2, 72-87, (2000)
[28] Hudson, T.; Lin, M.; Cohen, J.; Gottschalk, S.; Manocha, D., V-collide: accelerate collision detection for vrml, ()
[29] F. Ivančić, Modeling and analysis of hybrid systems, Ph.D. Dissertation, University of Pennsylvania, Philadelphia, PA, 2003.
[30] K.J. Kristoffersen, F. Laroussinie, K.G. Larsen, P. Pettersson, W. Yi, A compositional proof of a real-time mutual exclusion protocol, in: Proc. 7th Internat. Joint Conf. Theory and Practice of Software Development (TAPSOFT’97), Lille, France, April 1997, vol. 1214, Springer, Berlin, 1997, pp. 565-579.
[31] Larsen, K.; Pettersson, P.; Yi, W., U{\scppaal} in a nutshell, Springer internat. J. software tools technol. transfer, 1, (1997)
[32] Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S., Property preserving abstractions for the verification of concurrent systems, Formal meth. system des., 6, 1, (1995) · Zbl 0829.68053
[33] Megiddo, N., On the complexity of polyhedral separability, Discrete comput. geometry, 3, 325-337, (1988) · Zbl 0669.68035
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.