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:
Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

STL Model Checking of Continuous and Hybrid Systems

verfasst von : Hendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Signal Temporal Logic (STL) is a formalism for reasoning about temporal properties of continuous-time traces of hybrid systems. Previous work on this subject mostly focuses on robust satisfaction of an STL formula for a particular trace. In contrast, we present a method solving the problem of formally verifying an STL formula for continuous and hybrid system models, which exhibit uncountably many traces. We consider an abstraction of a model as an evolution of reachable sets. Through leveraging the representation of the abstraction, the continuous-time verification problem is reduced to a discrete-time problem. For the given abstraction, the reduction to discrete-time and our decision procedure are sound and complete for finitely represented reach sequences and sampled time STL formulas. Our method does not rely on a special representation of reachable sets and thus any reachability analysis tool can be used to generate the reachable sets. The benefit of the method is illustrated on an example from the context of automated driving.

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 Skolem Functions for DQBF
Nächstes Kapitel Clause Sharing and Partitioning for Cloud-Based SMT Solving
Literatur
1.
Ahmadyan, S.N., Kumar, J.A., Vasudevan, S.: Runtime verification of nonlinear analog circuits using incremental time-augmented RRT algorithm. In: Proceedings of Design, Test & Automation in Europe (2013)
2.
Althoff, M.: An introduction to CORA . In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120–151 (2015)
3.
Althoff, M., Dolan, J.M.: Reachability computation of low-order models for the safety verification of high-order road vehicle models. In: American Control Conference, pp. 3559–3566. IEEE (2012)
4.
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of 5th Symposium on Logic in Computer Science, pp. 414–425 (1990)
5.
6.
Asarin, E., et al.: Recent progress in continuous and hybrid reachability analysis. In: Conference on Computer Aided Control Systems Design, pp. 1582–1587 (2006)
7.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
8.
Bresolin, D.: HyLTL: a temporal logic for model checking hybrid systems. In: Proceedings Third International Workshop on Hybrid Autonomous Systems, pp. 73–84. HAS (2013)
9.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
10.
Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015)
11.
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRefMATH
12.
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Computer Aided Verification, pp. 379–395 (2011)
13.
Guéguen, H., Lefebvre, M., Zaytoon, J., Nasri, O.: Safety verification and reachability analysis for hybrid systems. Ann. Rev. Control 33(1), 25–36 (2009)CrossRef
14.
Lee, E.A.: CPS foundations. In: Design Automation Conference, pp. 737–742 (2010)
15.
Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Proceedings of the IntemationaI Conference on Parallel and Distributed Processing Techniques and Applications (1999)
16.
Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475–505. Springer, Heidelberg (2008)CrossRef
17.
Maler, O., Ničković, D.: Monitoring properties of analog and mixed-signal circuits. J. Softw. Tools Technol. Transfer 15, 247–268 (2013)CrossRef
18.
Mitra, S., Wongpiromsarn, T., Murray, R.M.: Verifying cyber-physical interactions in safety-critical systems. IEEE Secur. Priv. 11(4), 28–37 (2013)CrossRef
19.
Pinto, A., Sangiovanni-Vincentelli, A.L., Carloni, L.P., Passerone, R.: Interchange formats for hybrid systems: review and proposal. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 526–541. Springer, Heidelberg (2005)CrossRef
20.
Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473–486. Springer, Heidelberg (2007)CrossRef
21.
Poovendran, R.: Cyberphysical systems: close encounters between two parallel worlds. Proc. IEEE 98(8), 1363–1366 (2010)CrossRef
22.
Rajkumar, R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: Design Automation Conference, pp. 731–736 (2010)
23.
Sanwal, M.U., Hasan, O.: Formal verification of cyber-physical systems: coping with continuous elements. In: Proceedings of the 16th International Conference on Computational Science and its Applications, pp. 358–371 (2013)
24.
Sauter, G., Dierks, H., Fränzle, M., Hansen, M.R.: Lightweight hybrid model checking facilitating online prediction of temporal properties. In: Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT09, pp. 20–22 (2009)
25.
Smirnov, G.V.: Introduction to the Theory of Differential Inclusions. American Mathematical Society, Providence (2002)MATH
26.
Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Model-Based Testing and Monitoring for Hybrid Embedded Systems, pp. 487–492 (2004)
27.
Wang, Z., Zaki, M.H., Tahar, S.: Statistical runtime verification of analog and mixed signal designs. In: Conference on Signals, Circuits and Systems (2009)
Metadaten
Titel
STL Model Checking of Continuous and Hybrid Systems
verfasst von
Hendrik Roehm
Jens Oehlerking
Thomas Heinz
Matthias Althoff
Copyright-Jahr
2016
Buch
Automated Technology for Verification and Analysis

Print ISBN: 978-3-319-46519-7

Electronic ISBN: 978-3-319-46520-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46520-3_26