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:
ProCoS: How It All Began – as Seen from Denmark Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers

verfasst von : Ernst-Rüdiger Olderog, Anders P. Ravn, Rafael Wisniewski

Erschienen in: Provably Correct Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

The interplay between discrete and continuous dynamical models is discussed, and a systematic approach to developing and combining these models together is outlined. The combination is done with linking predicates that define refinement relations between the models. As a case study, we build an abstract, discr spatial model and a concrete, continuous dynamic model for traffic manoeuvrers of multiple vehicles on highways. In the discrete model we show the safety (collision freedom) of distance keeping and lane-change manoeuvrers using events and actions to specify state transitions. By linking the discrete and continuous model via suitable predicates that express the discrete events and actions as distances and set-points in the continuous model, the safety carries over to the concrete model.

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 A Proof Method for Linearizability on TSO Architectures
Nächstes Kapitel Towards Interface-Driven Design of Evolving Component-Based Architectures
Literatur
1.
Althoff, M., Stursberg, O., Buss, M.: Safety assessment of autonomous cars using verification techniques. In: American Control Conference (ACC) 2007, pp. 4154–4159. IEEE (2007)
2.
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetCrossRefMATH
3.
4.
Ames, A.D., Cousineau, E.A., Powell, M.J.: Dynamically stable bipedal robotic walking with nao via human-inspired hybrid zero dynamics. In: HSCC 2012, pp. 135–144. ACM (2012)
5.
Arechiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using theorem provers to guarantee closed-loop system properties. In: American Control Conference (ACC) 2012, pp. 3573–3580. IEEE (2012)
6.
Damm, W., Ihlemann, C., Sofroni-Stokkermans, V.: PTIME parametric verification of safety properties for reasonable linear hybrid systems. Math. Comput. Sci. 5(4), 469–497 (2011)MathSciNetCrossRefMATH
7.
Damm, W., Möhlmann, E., Rakow, A.: Component based design of hybrid systems: a case study on concurrency and coupling. In: HSCC 2014, pp. 145–150. ACM (2014)
8.
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, New York (1998)CrossRefMATH
9.
Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, London (2014)
10.
Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008)
11.
Fränzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form. Methods Syst. Des. 30(3), 179–198 (2007)CrossRefMATH
12.
13.
Frehse, G., Guernic, C., Donzé, A., Cotton, S., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
14.
15.
Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds).: Hybrid Systems. LNCS, vol. 736, Springer, Heidelberg (1993)
16.
Grumberg, O.: Abstraction and reduction in model checking. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliabilty. Nato Science Series II. Math., Physics and Chemistry, vol. 62, pp. 213–260. Kluwer Academic Publishers, Boston (2002)
17.
Habets, L., Collins, P., van Schuppen, J.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans. Autom. Control 51(6), 938–948 (2006)MathSciNetCrossRef
18.
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE (1996)
19.
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. STTT 1(1–2), 110–122 (1997)CrossRefMATH
20.
Hereid, A., Kolathaya, S., Jones, M.S., Van Why, J., Hurst, J.W., Ames, A.D.: Dynamic Multi-domain Bipedal Walking with Atrias Through Slip Based Human-Inspired Control. HSCC 2014. pp. 263–272, ACM (2014)
21.
Hilscher, M., Linker, S., Olderog, E.-R.: Proving safety of traffic manoeuvres on country roads. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 196–212. Springer, Heidelberg (2013)
22.
Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404–419. Springer, Heidelberg (2011)
23.
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, London (1998)
24.
Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. HSCC 2005, 25–53 (2005)
25.
Linker, S.: Proofs for traffic safety: combining diagrams and logic. Ph.D thesis, Dept. of. Comp. Sci, Univ. of Oldenburg (2015)
26.
27.
Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M.J., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42–56. Springer, Heidelberg (2011)
28.
Lygeros, J., Godbole, D.N., Sastry, S.S.: Verified hybrid controllers for automated vehicles. IEEE Trans. Autom. Control 43(4), 522–539 (1998)MathSciNetCrossRefMATH
29.
Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata revisited. HSCC 2001, 403–417 (2001)
30.
31.
Moor, T., Raisch, J., Davoren, J.: Admissiblity criteria for a hierarchical design of hybrid systems. In: Proceedings IFAD Conference on Analysis and Design of Hybrid Systems, pp. 389–394. St. Malo, France (2003)
32.
Moor, T., Raisch, J., O’Young, S.: Discrete supervisory control of hybrid systems based on l-complete approximations. Discret. Event Dyn. Syst. 12, 83–107 (2002)MathSciNetCrossRefMATH
33.
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18(2), 10–19 (1985)CrossRef
34.
Nadjm-Tehrani, S., Strömberg, J.: From physical modelling to compositional models of hybrid systems. In: Langmaack, H., de Roever, W.P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems – ProCoS, vol. 863 of LNCS, pp. 583–604. Springer (1994)
35.
Olderog, E.-R., Ravn, A., Wisniewski, R.: Linking spatial and dynamic models for traffic maneuvers. In: 54th IEEE Conference on Decision and Control (CDC), 8 pp. IEEE (2015)
36.
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Spinger, Heidelberg (2010)CrossRefMATH
37.
Rajamani, R.: Vehicle Dynamics and Control. Mechanical engineering series. Springer Science, New York (2006)MATH
38.
Rajhans, A., Krogh, B.H.: Compositional heterogeneous abstraction. In: HSCC 2013, pp. 253–262. ACM (2013)
39.
Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proceedings 3rd International Conference Knowledge Representation and Reasoning (1992)
40.
Schäfer, A.: A calculus for shapes in time and space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–478. Springer, Heidelberg (2005)
41.
Shao, Z., Liu, J.: Spatio-temporal hybrid automata for cyber-physical systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 337–354. Springer, Heidelberg (2005)
42.
Sreenath, K., Hill Jr., C.R., Kumar, V.: A partially observable hybrid system model for bipedal locomotion for adapting to terrain variations. In: HSCC 2013, pp. 137–142. ACM (2013)
43.
van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer, Netherlands (2007)CrossRef
44.
Varaija, P.: Smart cars on smart roads: problems of control. IEEE Trans. Autom. Control AC 38(2), 195–207 (1993)MathSciNetCrossRef
45.
Werling, M., Gindele, T., Jagszent, D., Gröll, L.: A robust algorithm for handling traffic in urban scenarios. In: Proceedings of IEEE Intelligent Vehicles Symposium, pp. 168–173. Eindhoven, NL (2008)
46.
Woodcock, J., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice Hall, New Jersey (1996)MATH
47.
48.
Zabczyk, J.: Mathematical Control Theory – An Introduction. Birkhäuser (2008)
49.
Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207–281. Springer, Heidelberg (2013)
50.
51.
Ziegler, J., Bender, P., Dang, T., Stiller, C.: Trajectory planning for bertha – A local, continuous method. In: 2014 IEEE Intelligent Vehicles Symposium Proceedings, Dearborn, MI, USA, June 8-11, 2014, pp. 450–457 (2014)
Metadaten
Titel
Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers
verfasst von
Ernst-Rüdiger Olderog
Anders P. Ravn
Rafael Wisniewski
Copyright-Jahr
2017
Buch
Provably Correct Systems

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

Electronic ISBN: 978-3-319-48628-4

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-48628-4_5