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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automated Theory Exploration for Interactive Theorem Proving: Kapitel lesen Erstes Kapitel lesen

2017 | Supplement | Buchkapitel

Bellerophon: Tactical Theorem Proving for Hybrid Systems

verfasst von : Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Hybrid systems combine discrete and continuous dynamics, which makes them attractive as models for systems that combine computer control with physical motion. Verification is undecidable for hybrid systems and challenging for many models and properties of practical interest. Thus, human interaction and insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing them to focus on those insights. We present a tactics language and library for hybrid systems verification, named Bellerophon, that provides a way to convey insights by programming hybrid systems proofs.
We demonstrate that in focusing on the important domain of hybrid systems verification, Bellerophon emerges with unique automation that provides a productive proving experience for hybrid systems from a small foundational prover core in the KeYmaera X prover. Among the automation that emerges are tactics for decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize the benefit of automated solvers and general-purpose heuristic proof search. Our presentation begins with syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification effort exploiting Bellerophon’s support for invariant and arithmetic reasoning for a non-solvable 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

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!

Jetzt informieren
Vorheriges Kapitel Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
Nächstes Kapitel Formalizing Basic Quaternionic Analysis
Fußnoten
1
A continuous evolution along the differential equation system \(x_i'=\theta _i\) for an arbitrary duration within the region described by formula F. The & F is optional so that e.g., \(\{x'=\theta \}\) is equivalent to \( \{x'=\theta \& \textit{true}\}\).
 
2
Tactics may map a single sequent to a list of sequents; the simplest example of such a tactic andR corresponds to the proof rule \(\wedge \text {R}\), which maps a single sequent \(\varGamma \vdash A \wedge B, \varDelta \) to the list of subgoals \(\varGamma \vdash A, \varDelta \) and \(\varGamma \vdash B, \varDelta \).
 
3
The addressing scheme extends to subformulas and subterms in a straight-forward way. Interested readers may refer to the Bellerophon documentation for details.
 
4
Tactic e is applicable at a position pos if e(pos) does not result in an error.
 
5
The attentive reader will notice we use g() instead of g. This is to indicate that the model has an arity 0 function symbol g(), rather than an assignable variable. This syntactic convention follows KeYmaera X and its predecessors.
 
6
Advanced automation generally uses the EDSL. Programs written in the EDSL are executed using the same interpreter as programs written in pure Bellerophon.
 
Literatur
1.
de Moura, L.M., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 378–388. Springer, Cham (2015). doi:10.​1007/​978-3-319-21401-6_​26CrossRef
2.
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., et al. (eds.) [13], pp. 209–229
3.
Barras, B., Carmen González Huesca, L., Herbelin, H., Régis-Gianas, Y., Tassi, E., Wenzel, M., Wolff, B.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 359–363. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39320-4_​29CrossRef
4.
Bohrer, R., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, pp. 208–221. ACM (2017)
5.
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRef
6.
Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)MATH
7.
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)MathSciNetCrossRef
8.
Constable, R.L., Allen, S.F., Bromley, M., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Upper Saddle River (1986)
9.
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)MathSciNetCrossRef
10.
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263–279 (2008)CrossRef
11.
12.
Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 527–538. Springer, Cham (2015). doi:10.​1007/​978-3-319-21401-6_​36CrossRef
13.
14.
15.
Hickey, J., et al.: MetaPRL – a modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287–303. Springer, Heidelberg (2003). doi:10.​1007/​10930755_​19CrossRef
16.
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39634-2_​21CrossRef
17.
18.
Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​15CrossRef
19.
Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1) (2011)
20.
21.
Mitsch, S., Platzer, A.: The KeYmaera X proof IDE: concepts on usability in hybrid systems theorem proving. In: FIDE-3. EPTCS, vol. 240, pp. 67–81 (2016)
22.
Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des. 49(1), 33–74 (2016). Special issue of selected papers from RV’14CrossRef
23.
24.
25.
26.
Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13–24. IEEE (2012)
27.
Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–266 (2017)MathSciNetCrossRef
28.
Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Form. Methods Syst. Des. 35(1), 98–120 (2009). Special issue for selected papers from CAV’08CrossRef
29.
Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 171–178. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-71070-7_​15CrossRef
30.
31.
Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383–397. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38088-4_​26CrossRef
Metadaten
Titel
Bellerophon: Tactical Theorem Proving for Hybrid Systems
verfasst von
Nathan Fulton
Stefan Mitsch
Rose Bohrer
André Platzer
Copyright-Jahr
2017
Verlag
Springer International Publishing
Buch
Interactive Theorem Proving

Print ISBN: 978-3-319-66106-3

Electronic ISBN: 978-3-319-66107-0

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66107-0_14

Premium Partner

    Bildnachweise