nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

02.05.2022 | General

Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns

verfasst von: Yanni Kouskoulas, T. J. Machado, Daniel Genin, Aurora Schmidt, Ivan Papusha, Joshua Brulé

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 3/2022

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We present an approach to analyze the safety of asynchronous, independent, non-deterministic, turn-to-bearing horizontal maneuvers for two vehicles. Future turn rates, final bearings, and continuously varying ground speeds throughout the encounter are unknown but restricted to known ranges. We develop a library of formal proofs about turning kinematics and apply the library to create a formally verified timing computation. Additionally, we create a technique that evaluates future collision possibilities that is based on waves of position possibilities and relies on the timing computation. The result either determines that the encounter will be collision-free, or computes a safe overapproximation for when and where collisions may occur.

Vorheriger Artikel Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods

Nächster Artikel Verifiable strategy synthesis for multiple autonomous agents: a scalable approach

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

Coq proofs are at https://bitbucket.org/ykouskoulas/ottb-foundation-proofs

There exist alternate expressions for this angle, but to our knowledge, the formulation in this paper is new.

Abhishek, A., Sood, H., Jeannin, J.B.: In: Formal verification of braking while swerving in automobiles. Association for computing machinery. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC ’20. Association for Computing Machinery, New York, NY, USA (2020)

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

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages, pp. 134–183. Springer (1975)

Cons, M.S., Shima, T., Domshlak, C.: Integrating task and motion planning for unmanned aerial vehicles. Unmanned Syst. 02(01), 19–38 (2014). https://doi.org/10.1142/S2301385014500022CrossRef

Fotiou, I.A., Rostalski, P., Parrilo, P.A., Morari, M.: Parametric optimization and optimal control using algebraic geometry methods. Int. J. Control 79(11), 1340–1358 (2006)MathSciNetCrossRef

Genin, D., Papusha, I., Brulé, J., Young, T., Mullins, G., Kouskoulas, Y., Wu, R., Schmidt, A.: Formal verification of neural network controllers for collision-free flight. In: 14th International Workshop on Numerical Software Verification (NSV) (2021)

Isaiah, P., Shima, T.: A task and motion planning algorithm for the Dubins travelling salesperson problem. IFAC Proc. Vol. 47(3), 9816–9821 (2014). (19th IFAC World Congress)CrossRef

Jeannin, J., Ghorbal, K., Kouskoulas, Y., Schmidt, A., Gardner, R., Mitsch, S., Platzer, A.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT 19(6), 717–741 (2017). https://doi.org/10.1007/s10009-016-0434-1CrossRef

Jeyaraman, S., Tsourdos, A., Żbikowski, R., White, B.A.: Formal techniques for the modelling and validation of a co-operating uav team that uses dubins set for path planning. In: Proceedings of the 2005, American Control Conference, 2005, vol. 7, pp. 4690–4695 (2005)

10.

Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving—8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, pp. 336–353. Springer (2017)

11.

12.

Kouskoulas, Y., Machado, T.J., Genin, D.: Formally verified timing computation for non-deterministic horizontal turns during aircraft collision avoidance maneuvers. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems—25th International Conference, FMICS 2020, Vienna, Austria, September 2–3, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12327, pp. 113–129. Springer (2020)

13.

Kouskoulas, Y., Schmidt, A., Jeannin, J.B., Genin, D., Lopez, J.: Provably safe controller synthesis using safety proofs as building blocks. In: IEEE 7th International Conference on Software Engineering Research and Innovation, CONISOFT 2019, October 23–25, 2019, Mexico City, Mexico, pp. 26–35 (2019)

14.

Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796–817 (2001)MathSciNetCrossRef

15.

LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)CrossRef

16.

Ma, X., Castanon, D.A.: Receding horizon planning for Dubins traveling salesman problems. In: Proceedings of the 45th IEEE Conference on Decision and Control, pp. 5453–5458 (2006)

17.

McGee, T.G., Hedrick, J.K.: Path planning and control for multiple point surveillance by an unmanned aircraft in wind. In: 2006 American Control Conference, pp. 4261–4266 (2006)

18.

Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36(12), 1312–1340 (2017). https://doi.org/10.1177/0278364917733549CrossRef

19.

Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)MathSciNetCrossRef

20.

Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1-19:44 (2017). https://doi.org/10.1145/3091123

21.

Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D. (eds.) FM, LNCS, vol. 5850, pp. 547–562. Springer (2009). https://doi.org/10.1007/978-3-642-05089-3_35

22.

Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: IEEE Conference on Decision and Control, vol. 1, pp. 741–746 (2002)

23.

Song, X., Hu, S.: 2d path planning with Dubins-path-based A\(\star \) algorithm for a fixed-wing UAV. In: 3rd IEEE International Conference on Control Science and Systems Engineering (ICCSSE), Beijing, China, pp. 69–73 (2017)

24.

The Coq proof assistant. https://coq.inria.fr (2020). Accessed 24 May 2020

25.

Wu, A., How, J.: Guaranteed infinite horizon avoidance of unpredictable, dynamically constrained obstacles. Auton. Robots 32(3), 227–242 (2012)

26.

Zhao, Z., Yang, J., Niu, Y., Zhang, Y., Shen, L.: A hierarchical cooperative mission planning mechanism for multiple unmanned aerial vehicles. Electronics 8, 443 (2019). https://doi.org/10.3390/electronics8040443CrossRef

Titel: Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns
verfasst von: Yanni Kouskoulas
T. J. Machado
Daniel Genin
Aurora Schmidt
Ivan Papusha
Joshua Brulé
Publikationsdatum: 02.05.2022
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 3/2022
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-022-00654-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 3/2022

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods

DivSIM , an interactive simulator for LLVM bitcode

Temporal-logic query checking over finite data streams

Verifiable strategy synthesis for multiple autonomous agents: a scalable approach

Formal verification of OIL component specifications using mCRL2

Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture

Premium Partner