×

zbMATH — the first resource for mathematics

Hybrid automata-based CEGAR for rectangular hybrid systems. (English) Zbl 1341.68109
Summary: In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well, as opposed to finite state systems. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. The experimental evaluations demonstrate the merits of the approach.

MSC:
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification, vol 1855 of Lecture Notes in Computer Science. pp 154-169 · Zbl 0974.68517
[2] Ball T, Rajamani S (2000) Bebop: a symbolic model checker for Boolean programs. In: Proceedings of the 7th international SPIN, pp 113-130 · Zbl 0976.68540
[3] Corbett J, Dwyer M, Hatcliff J, Laubach S, Robby C. Pasareanu, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of ICSE. pp 439-448
[4] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy Abstraction. In: Proceedings of 29th ACM symposium on principles of programming languages (POPL’02). pp 58-70 · Zbl 1323.68374
[5] Holzmann, G; Smith, M, Automating software feature verification, Bell Labs Tech J, 5, 72-87, (2000)
[6] Alur R, Dang T, Ivancic F (2003) Counter-example guided predicate abstraction of hybrid systems. In: Proceedings of TACAS 2003. pp 208-223 · Zbl 1031.68074
[7] Clarke, EM; Fehnker, A; Han, Z; Krogh, B; Ouaknine, J; Stursberg, O; Theobald, M, Abstraction and counterexample-guided refinement in model checking of hybrid systems, JFCS, 14, 583-604, (2003) · Zbl 1101.68678
[8] Clarke E.M., Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexmple-guided abstraction refinement. In: Proceedings of TACAS. pp 192-207 · Zbl 1031.68078
[9] Dierks H, Kupferschmid S, Larsen KG (2007) Automatic Abstraction refinement for timed automata. In: Proceedings of FORMATS. pp 114-129 · Zbl 1141.68431
[10] Fehnker A, Clarke EM, Jha S, Krogh B (2005) Refining abstractions of hybrid systems using counterexample fragments. In: Proceedings of HSCC 2005. pp 242-257 · Zbl 1078.93041
[11] Segelken M (2007) Abstraction and Counterexample-guided construction of omega-automata for model checking of step-discrete linear hybrid models. In: Proceedings of CAV. pp 433-448 · Zbl 1135.68482
[12] Sorea M (2004) Lazy approximation for dense real-time systems. In: Proceedings of FORMATS/FTRFTS. pp 363-378 · Zbl 1109.68507
[13] Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8 · Zbl 1078.93508
[14] Graf S, Saidi H (1997) Construction of abstact state graphs with PVS. In: Proceedings of CAV, pp 72-83
[15] Jha SK, Krogh BH, Weimer JE, Clarke EM (2007) Reachability for linear hybrid automata using iterative relaxation abstraction. In: Proceedings of HSCC 2007, pp 287-300 · Zbl 1221.93115
[16] Henzinger TA (1996) The theory of hybrid automata. In: LICS, pp 278-292
[17] Hybrid abstraction refinement engine (HARE) (2013). In: http://publish.illinois.edu/hare-tool/
[18] Henzinger TA, Ho P-H, Howard W-T (1997) Hytech: a model checker for hybrid systems. In: Proceedings of CAV. pp 460-483 · Zbl 1060.68603
[19] Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Proceedings of HSCC. pp 258-273 · Zbl 1078.93533
[20] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In Proceedings of CAV
[21] Asarin E, Dang T, Maler O (2002) The d/dt tool for verification of hybrid system · Zbl 1010.68796
[22] Prabhakar P, Duggirala PS, Mitra S, Viswanathan M (2013) Hybrid automata-based cegar for rectangular hybrid systems. In: Proceedings of VMCAI. pp 48-67 · Zbl 1426.68175
[23] Doyen L, Henzinger TA, Raskin J-F (2005) Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS05, vol 3829 in LNCS. pp 144-161 · Zbl 1175.68243
[24] Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) What’s decidable about hybrid automata? In: Proceedings of STOC. pp 373-382 · Zbl 0978.68534
[25] Alur, Rajeev; Courcoubetis, Costas; Halbwachs, Nicolas; Henzinger, Thomas A; Ho, P-H; Nicollin, Xavier; Olivero, Alfredo; Sifakis, Joseph; Yovine, Sergio, The algorithmic analysis of hybrid systems, TCS, 138, 3-34, (1995) · Zbl 0874.68206
[26] Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. pp 326-341 · Zbl 1135.93324
[27] Munoz CA, Dowek G, Carreo V (2004) Modeling and verification of an air traffic concept of operations. In: ISSTA, pp 175-182
[28] Dutertre B, Sorea M (2004) Timed systems in SAL. Technical report, Computer Science Laboratory
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.