Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 2/2015

01-04-2015

Hybrid automata-based CEGAR for rectangular hybrid systems

Authors: Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan

Published in: Formal Methods in System Design | Issue 2/2015

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.
next article Optimization techniques for craig interpolant compaction in unbounded model checking

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Literature
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
2.
Ball T, Rajamani S (2000) Bebop: a symbolic model checker for Boolean programs. In: Proceedings of the 7th international SPIN, pp 113–130
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
5.
Holzmann G, Smith M (2000) Automating software feature verification. Bell Labs Tech J 5(2):72–87CrossRef
6.
Alur R, Dang T, Ivancic F (2003) Counter-example guided predicate abstraction of hybrid systems. In: Proceedings of TACAS 2003. pp 208–223
7.
Clarke EM, Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Abstraction and counterexample-guided refinement in model checking of hybrid systems. JFCS 14(4):583–604MATHMathSciNet
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
9.
Dierks H, Kupferschmid S, Larsen KG (2007) Automatic Abstraction refinement for timed automata. In: Proceedings of FORMATS. pp 114–129
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
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
12.
Sorea M (2004) Lazy approximation for dense real-time systems. In: Proceedings of FORMATS/FTRFTS. pp 363–378
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
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
16.
Henzinger TA (1996) The theory of hybrid automata. In: LICS, pp 278–292
17.
18.
Henzinger TA, Ho P-H, Howard W-T (1997) Hytech: a model checker for hybrid systems. In: Proceedings of CAV. pp 460–483
19.
Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Proceedings of HSCC. pp 258–273
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
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
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
24.
Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) What’s decidable about hybrid automata? In: Proceedings of STOC. pp 373–382
25.
Alur Rajeev, Courcoubetis Costas, Halbwachs Nicolas, Henzinger Thomas A, Ho P-H, Nicollin Xavier, Olivero Alfredo, Sifakis Joseph, Yovine Sergio (1995) The algorithmic analysis of hybrid systems. TCS 138(1):3–34CrossRefMATH
26.
Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. pp 326–341
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
Metadata
Title
Hybrid automata-based CEGAR for rectangular hybrid systems
Authors
Pavithra Prabhakar
Parasara Sridhar Duggirala
Sayan Mitra
Mahesh Viswanathan
Publication date
01-04-2015
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 2/2015
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-015-0225-4

Premium Partner

    Image Credits