Abstract
We develop a library of proofs to support rigorous mathematical reasoning about horizontal aircraft turning maneuvers, and apply it to formally verify a timing computation for use during mixed horizontal and vertical aircraft collision avoidance maneuvers. We consider turns that follow non-deterministic circular turn-to-bearing horizontal motion, formalizing path-length and timing properties. These kinematics are the building blocks for Dubins trajectories, and can be used to formalize a variety of techniques, including those that contain non-determinism. The timing computation establishes, for intersecting trajectories, the exact bounds of time intervals when the horizontal position of the aircraft might coincide, and during which they must be at different altitudes to avoid collision.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Change history
29 August 2020
In the originally published version of chapter 4 Equations 29 and 30 had the wrong guard expressions. This has now been corrected.
Notes
- 1.
Coq proofs are at https://bitbucket.org/ykouskoulas/ottb-foundation-proofs.
- 2.
There exist alternate expressions for this angle, but to our knowledge, the formulation in this paper is new.
References
The coq proof assistant. https://coq.inria.fr. Accessed 24 May 2020
Abhishek, A., Sood, H., Jeannin, J.-B.: Formal verification of braking while swerving in automobiles. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020. Association for Computing Machinery, New York (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). https://doi.org/10.1007/s11786-014-0181-1
Cons, M.S., Shima, T., Domshlak, C.: Integrating task and motion planning for unmanned aerial vehicles. Unmanned Syst. 02(01), 19–38 (2014)
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
Jeannin, J.-B., et al.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT 19(6), 717–741 (2017)
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)
Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.-B.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 336–353. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_22
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, December 2006
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, p. 6, June 2006
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)
Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1–19:44 (2017)
Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_35
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Kouskoulas, Y., Machado, T.J., Genin, D. (2020). Formally Verified Timing Computation for Non-deterministic Horizontal Turns During Aircraft Collision Avoidance Maneuvers. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-58298-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-58297-5
Online ISBN: 978-3-030-58298-2
eBook Packages: Computer ScienceComputer Science (R0)