Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
C4C Case Studies Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

39. An Introduction to the Verification of Hybrid Systems Using Ariadne

verfasst von : Davide Bresolin, Luca Geretti, Tiziano Villa, Pieter Collins

Erschienen in: Coordination Control of Distributed Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We introduce the verification of hybrid systems as offered by the open-source framework called ARIADNE. The ARIADNE C++ library exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms based on reachability analysis. We demonstrate the tool using a classical example of a controlled water tank system.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Nonanticipative Duality of Sources and Channels with Memory and Feedback
Nächstes Kapitel Formal Verification Applied to Robotic Surgery
Fußnoten
1
ImageSets are used in the stable version of Ariadne. The development version uses a more accurate representation based on ConstrainedImageSets [7].
 
Literatur
1.
Alur R, Courcoubetis C, Henzinger TA, Ho PH (1992) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, LNCS. Springer, Berlin, pp 209–229
2.
Alur Rajeev, Dang Thao, Ivančić Franjo (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250–271
3.
4.
Benvenuti L, Bresolin D, Collins P, Ferrari A, Geretti L, Villa T (2012) Ariadne: Dominance checking of nonlinear hybrid automata using reachability analysis. Reachability Problems., volume 7550 of LNCSSpringer, Berlin Heidelberg, pp 79–91
5.
Benvenuti L, Bresolin D, Collins P, Ferrari A, Geretti L, Villa T (2014) Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int J Robust Nonlinear Control 24(4):699–724
6.
Bresolin D (2013) Improving HyLTL model checking of hybrid systems. In: Proceedings of the 4th international symposium on games, automata, logics and formal verification (GandALF2013), vol 119 of EPTCS, pp 79–92
7.
Collins P, Bresolin D, Geretti L, Villa T (2012) Computing the evolution of hybrid systems using rigorous function calculus. In: Proceedings of the 4th IFAC conference on analysis and design of Hybrid Systems (ADHS12), pp 284–290
8.
Frehse G (2008) PHAVer: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf (STTT) 10:263–279
9.
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 23rd international conference on computer aided verification (CAV 2011), volume 6806 of LNCS. Springer, Berlin, pp 379–395
10.
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1)
11.
Tomlin CJ, Lygeros J, Sastry SS (2000) A game theoretic approach to controller design for hybrid systems. Proc IEEE 88(7):949–970
Metadaten
Titel
An Introduction to the Verification of Hybrid Systems Using Ariadne
verfasst von
Davide Bresolin
Luca Geretti
Tiziano Villa
Pieter Collins
Copyright-Jahr
2015
Buch
Coordination Control of Distributed Systems

Print ISBN: 978-3-319-10406-5

Electronic ISBN: 978-3-319-10407-2

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-10407-2_39

Neuer Inhalt

    Bildnachweise