Hostname: page-component-848d4c4894-p2v8j Total loading time: 0 Render date: 2024-05-07T16:02:31.925Z Has data issue: false hasContentIssue false
  • English
  • Français

Can we build it: formal synthesis of control strategies for cooperative driver assistance systems†

Published online by Cambridge University Press:  08 July 2013

WERNER DAMM ,
HANS-JÖRG PETER ,
JAN RAKOW  and
BERND WESTPHAL
WERNER DAMM
Affiliation:
Carl von Ossietzky Universität Oldenburg, Interdisciplinary Research Centre on Safety Critical Systems and OFFIS Transportation, Germany Email: damm@offis.de
HANS-JÖRG PETER
Affiliation:
Universität des Saarlandes, Germany Email: peter@cs.uni-saarland.de
JAN RAKOW
Affiliation:
Carl von Ossietzky Universität Oldenburg, Germany Email: jan.rakow@informatik.uni-oldenburg.de
BERND WESTPHAL
Affiliation:
Albert-Ludwigs-Universität Freiburg, Germany Email: westphal@informatik.uni-freiburg.de
Get access Rights & Permissions [Opens in a new window]

Abstract

We propose a design and verification methodology supporting the early phases of system design for cooperative driver assistance systems, focusing on the realisability of new automotive functions. Specifically, we focus on applications where drivers are supported in complex driving tasks by safe strategies involving the coordinated movements of multiple vehicles to complete the driving task successfully. We propose a divide and conquer approach for formally verifying timed probabilistic requirements on successful completion of the driving task and collision freedom based on formal specifications of a set of given manoeuvring and communication capabilities of the car. In particular, this allows an assessment of whether they are sufficient to implement strategies for successful completion of the driving task.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Special Issue 4: Lightweight and Practical Formal Methods in the Design and Analysis of Safety-Critical Systems , August 2013 , pp. 676 - 725
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This research was partially supported by the German Science Foundation within the Transregional Collaborative Research Centre TR14 AVACS and the VW-Vorab Research Group IMOST.

References

Althoff, M., Stursberg, O. and Buss, M. (2007) Online verification of cognitive car decisions. In: Intelligent Vehicles Symposium, IEEE 728–733.Google Scholar
Althoff, M., Stursberg, O. and Buss, M. (2008) Verification of uncertain embedded systems by computing reachable sets based on zonotopes. In: Proceedings of the 17th IFAC World Congress 5125–5130.CrossRefGoogle Scholar
Alur, R., Courcoubetis, C., Henzinger, T. A. and Ho, P.-H. (1992) Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R. L., Nerode, A., Ravn, A. P. and Rischel, H., (eds.) Hybrid Systems. Springer-Verlag Lecture Notes in Computer Science 736 209–229.CrossRefGoogle Scholar
Alur, R., Henzinger, T. A. and Kupferman, O. (2002) Alternating-time temporal logic. Journal of the ACM 49 (5)672–713.CrossRefGoogle Scholar
Alur, R., Madhusudan, P. and Nam, W. (2005) Symbolic computational techniques for solving games. Software Tools for Technology Transfer: STTT 7 (2)118–128.CrossRefGoogle Scholar
Baldessari, R.et al. (2007) Car-2-car communication consortium – manifesto.Google Scholar
Baskar, D. (2009) Traffic Management and Control in Intelligent Vehicle Highway Systems, Ph.D. thesis, University of Delft.Google Scholar
Bauer, J., Schaefer, I., Toben, T. and Westphal, B. (2006) Specification and verification of dynamic communication systems. In: Proceedings of Sixth International Conference on Application of Concurrency to System Design: ACSD 2006, IEEE 189–200.CrossRefGoogle Scholar
Bauer, J., Toben, T. and Westphal, B. (2007) Mind the shapes: abstraction refinement via topology invariants. In: Namjoshi, K. S., Yoneda, T., Higashino, T. and Okamura, Y. (eds.) Proceedings of the 5th international conference on automated technology for verification and analysis: ATVA'07. Springer-Verlag Lecture Notes in Computer Science 4762 35–50.CrossRefGoogle Scholar
Bellemans, T., De Schutter, B. and De Moor, B. (2006) Model predictive control for ramp metering of motorway traffic: A case study. Control Engineering Practice 14 (7)757–767.CrossRefGoogle Scholar
Bianco, A. and de Alfaro, L. (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P. (ed.) Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 1026 499–513.CrossRefGoogle Scholar
Brockmeyer, U. (1999) Verifikation von Statemate Designs, Ph.D. thesis, Carl von Ossietzky Universität Oldenburg.Google Scholar
Broucke, M. and Varaiya, P. (1997) The automated highway system: A transportation technology for the 21st century. Control Engineering Practice 5 (11)1583–1590.CrossRefGoogle Scholar
Damm, W. and Finkbeiner, B. (2011) Does it pay to extend the perimeter of a world model? In: Proceedings of the 17th International Symposium on Formal Methods.CrossRefGoogle Scholar
Damm, W., Dierks, H., Oehlerking, J. and Pnueli, A. (2010) Towards component based design of hybrid systems: Safety and stability. In: Manna, Z. and Peled, D. (eds.) Essays in Memory of Amir Pnueli. Springer-Verlag Lecture Notes in Computer Science 6200 96–143.CrossRefGoogle Scholar
Damm, W., Ihlemann, C. and Sofronie-Stokkermans, V. (2011b) Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata. In: Frazzoli, E. and Grosu, R. (eds.) Proceedings of the 14th international conference on Hybrid systems: computation and control: HSCC '11, ACM 73–82.Google Scholar
Damm, W.et al. (2006a) Automatic verification of hybrid systems with large discrete state space. In: Graf, S. and Zhang, W. (eds.) Automated Technology for Verification and Analysis – Proceedings 4th International Symposium, ATVA 2006. Springer-Verlag Lecture Notes in Computer Science 4218 276–291.CrossRefGoogle Scholar
Damm, W.et al. (2006b) Automatic verification of hybrid systems with large discrete state space. In: Proceedings of the 4th Symposium on Automated Technology for Verification and Analysis. Springer-Verlag Lecture Notes in Computer Science 4218 276–291.CrossRefGoogle Scholar
Damm, W.et al. (2007) Exact state set representations in the verification of linear hybrid systems with large discrete state space. In: Namjoshi, K. S., Yoneda, T., Higashino, T. and Okamura, Y. (eds.) Proceedings of the 5th international conference on Automated technology for verification and analysis: ATVA'07. Springer-Verlag Lecture Notes in Computer Science 4762 425–440.CrossRefGoogle Scholar
Damm, W.et al. (2011a) Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces,. Science of Computer Programming, Special Issue on Automated Verification of Critical Systems. 77 (10–11)1122–1150.Google Scholar
Ehlers, R. (2010) Symbolic bounded synthesis. In: Touili, T., Cook, B. and Jackson, P. (eds.) CAV. Springer-Verlag Lecture Notes in Computer Science 6174 365–379.CrossRefGoogle Scholar
Ehlers, R. (2011) Unbeast: Symbolic bounded synthesis. In: Abdulla, P. A. and Leino, K R. M. (eds.) TACAS. Springer-Verlag Lecture Notes in Computer Science 6605 272–275.CrossRefGoogle Scholar
Ehlers, R.et al. (2011) Dynamic communicating probabilistic timed automata playing games. Reports of SFB/TR 14 AVACS 75, SFB/TR 14 AVACS. ISSN: 1860-9821 (Available at http://www.avacs.org.)Google Scholar
Eichler, S. (2009) Solutions for Scalable Communication and System Security in Vehicular Network Architectures, Ph.D. thesis, Technische Universität München.Google Scholar
Frehse, G. (2005) Phaver: Algorithmic verification of hybrid systems past hytech. In: Morari, M. and Thiele, L. (eds.) HSCC. Springer-Verlag Lecture Notes in Computer Science 3414 258–273.CrossRefGoogle Scholar
Frehse, G. (2006) On timed simulation relations for hybrid systems and compositionality. In: Asarin, E. and Bouyer, P. (eds.) FORMATS. Springer-Verlag Lecture Notes in Computer Science 4202 200–214.CrossRefGoogle Scholar
Frehse, G. (2008) Phaver: algorithmic verification of hybrid systems past hytech. Software Tools for Technology Transfer: STTT 10 (3)263–279.CrossRefGoogle Scholar
Frese, C. (2010) A comparison of algortihms for planning cooperative motions. Technical Report IES-2010-14, Lehrstuhl für Interaktive Echtzeitsysteme.Google Scholar
Frese, C., Batz, T., Wieser, M. and Beyerer, J. (2008) Life cycle management for cooperative groups of cognitive automobiles in a distributed environment. In: Intelligent Vehicles Symposium, 2008, IEEE 1125–1130.CrossRefGoogle Scholar
Frese, C. and Beyerer, J. (2010) Planning cooperative motions of cognitive automobiles using tree search algorithms. In: Dillmann, R., Beyerer, J., Hanebeck, U. D. and Schultz, T. (eds.) KI 2010: Advances in Artificial Intelligence. Springer-Verlag Lecture Notes in Computer Science 6359 91–98.CrossRefGoogle Scholar
Hansson, H. and Jonsson, B. (1994) A logic for reasoning about time and reliability. Formal Aspects of Computing 6 102–111.CrossRefGoogle Scholar
Henzinger, T. A., Ho, P.-H. and Wong-toi, H. (1996) Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43 225–238.Google Scholar
Henzinger, T. A., Minea, M. and Prabhu, V. S. (2001) Assume-guarantee reasoning for hierarchical hybrid systems. In: Benedetto, M D. D. and Sangiovanni-Vincentelli, A. L. (eds.) HSCC. Springer-Verlag Lecture Notes in Computer Science 2034 275–290.CrossRefGoogle Scholar
Henzinger, T. A. and Prabhu, V. S. (2006) Timed alternating-time temporal logic. In: Asarin, E. and Bouyer, P. (eds.) FORMATS. Springer-Verlag Lecture Notes in Computer Science 4202 1–17.CrossRefGoogle Scholar
Hsu, A., Eskafi, F., Sachs, S. and Varaiya, P. (1991) The design of platoon maneuver protocols for IVHS. PATH Report UCB-ITS-PRR-91-6, University of California.CrossRefGoogle Scholar
Kukimoto, Y. (1996) Blif-mv. Technical report, The VIS group, University of California, Berkeley.Google Scholar
Lee, K. (2008) Advanced research for integrated active transportation system. In: The National Workshop on New Research Directions for High Confidence Transportation Cyber Physical Systems, Washington, D.C., U.S.A.Google Scholar
Lygeros, J. and Lynch, N. A. (1998) Strings of vehicles: Modeling and safety conditions. In: Henzinger, T. A. and Sastry, S. (eds.) Proceedings Hybrid Systems: Computation and Control, First International Workshop, HSCC'98. Springer-Verlag Lecture Notes in Computer Science 1386 273–288.CrossRefGoogle Scholar
Lygeros, J., Tomlin, C. and Sastry, S. (1997) Multiobjective hybrid controller synthesis. In: Maler, O. (ed.) HART. Springer-Verlag Lecture Notes in Computer Science 1201 109–123.CrossRefGoogle Scholar
Pnueli, A. and Rosner, R. (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages: POPL'89 179–190.CrossRefGoogle Scholar
Richards, A. and How, J. (2002) Aircraft trajectory planning with collision avoidance using mixed integer linear programming. In: Proceedings of the American Control Conference, 2002, volume 3 1936–1941.CrossRefGoogle Scholar
Schewe, S. and Finkbeiner, B. (2007) Bounded synthesis. In: Namjoshi, K. S., Yoneda, T., Higashino, T. and Okamura, Y. (eds.) Proceedings of the 5th international conference on Automated technology for verification and analysis: ATVA'07. Springer-Verlag Lecture Notes in Computer Science 4762 474–488.CrossRefGoogle Scholar
Silva, B., Richeson, K., Krogh, B. and Chutinan, A. (2000) Modeling and verifying hybrid dynamic systems using CheckMate. In: Proceedings Conference on Automation of Mixed Processes: Hybrid Dynamic Systems 323–328.Google Scholar
Somenzi, F. (2009) CUDD: CU Decision Diagram package release 2.4.2.Google Scholar
Tabuada, P., Pappas, G. J. and Lima, P. U. (2004) Compositional abstractions of hybrid control systems. Discrete Event Dynamic Systems 14 (2)203–238.CrossRefGoogle Scholar
Tomlin, C., Lygeros, J. and Sastry, S. (1998a) Synthesizing controllers for nonlinear hybrid systems. In: Henzinger, T. A. and Sastry, S. (eds.) Proceedings Hybrid Systems: Computation and Control, First International Workshop, HSCC'98. Springer-Verlag Lecture Notes in Computer Science 1386 360–373.CrossRefGoogle Scholar
Tomlin, C., Pappas, G., Kosecka, J., Lygeros, J. and Sastry, S. (1998b) Advanced air traffic automation: A case study in distributed decentralized control. In: Siciliano, B. and Valavanis, K. (eds.) Control Problems in Robotics and Automation. Springer-Verlag Lecture Notes in Control and Information Sciences 230 261–295.CrossRefGoogle Scholar
Tomlin, C., Pappas, G. J., Lygeros, J., Godbole, D. N. and Sastry, S. (1996) Hybrid control models of next generarion air traffic management. In: Antsaklis, P. J., Kohn, W., Nerode, A. and Sastry, S. (eds.) Hybrid Systems. Springer-Verlag Lecture Notes in Computer Science 1273 378–404.CrossRefGoogle Scholar
Wachter, B. and Westphal, B. (2007) The spotlight principle. On combining process-summarising state abstractions. In: Cook, B. and Podelski, A. (eds.) VMCAI. Springer-Verlag Lecture Notes in Computer Science 4349 182–198.CrossRefGoogle Scholar
Westphal, B. (2008) Specification and Verification of Dynamic Topology Systems, Ph.D. thesis, Carl von Ossietzky Universität Oldenburg.Google Scholar
Wirtz, B., Strazny, T., Rakow, A. and Rakow, J. (2011) A lane change assistance system: Cooperation and hybrid control. Reports of SFB/TR 14 AVACS SFB/TR 14 AVACS.Google Scholar
Wittich, G. (1999) Ein problemorientierter Ansatz zum Nachweis von Realzeiteigenschaften eingebetteter Systeme, Ph.D. thesis, Carl von Ossietzky Universität Oldenburg.Google Scholar