Abstract
This paper describes a methodology for the design of flight plans for rotary-wing unmanned aerial vehicles based on formal verification. The methodology uses linear hybrid automata to model the aircraft which will be used to perform a given mission, the flight plan that will be executed by that aircraft, the region where the flight will be performed and the meteorological conditions expected at the time the flight will be performed. The resulting model can be formally verified with respect to previously established safety and timeliness requirements, like not running out of fuel or kee** minimum distances from ground during all phases of the mission. The result of this verification can be used to instantiate values in a parameterized flight plan or to assist an operator in incrementally constructing a flight plan whose feasibility can be guaranteed in advance. The methodology is being embedded in a graphical flight plan editor which greatly reduces the time needed to plan a mission and increases the safety of the aircraft’s operation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, and S. Yovine. The algorithmic analysis of hybrid systems. In Proceedings of the 11th International Conference on Analysis and Optimization of Discrete Event Systems, pages 331–351. Springer Verlag, 1994.
R. Alur, C. Courcoubetis, T. Henzinger, and P. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 209–229. Springer Verlag, 1993.
R. Alur, T. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3), March 1996.
David A. Fulghum. Outrider UAV tackles army, navy requirements. Aviation Week & Space Techology, July 22 1996.
T. Henzinger and P. Ho. HyTech: The Cornell HYbrid TECHnology tool. In Proceedings of 1994 Workshop on Hybrid Systems and Autonomous Control. Springer Verlag, 1995.
T. Henzinger, P. Ho, and H. Wong-Toi. A user guide to HyTech. In TACAS’95: Tools and Algorithms for the Construction and Analysis of Systems. Springer Verlag, 1995.
Pei-Hsin Ho. Automatic Analysis of Hybrid Systems. PhD thesis, Cornell University, Department of Computer Science, 1995.
S. Kandebo. CYPHER moves toward autonomous flight. Aviation Week & Space Techology, March 7 1994.
Gyron Sistemas Autônomos Ltda. Projeto HELIX: Definição e descryç ão geral. Internal document, unpublished, 1992.
NASA. Extending the vision. Unmanned Systems, 11(1), 1993.
X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 149–178. Springer Verlag, 1993.
C. Seibel and J.M. Farines. Formal verification and dimensioning of flight plans for rotary-wing unmanned aerial vehicles. In Proceedings of the 24th Annual Technical Symposium of the Association for Unmanned Vehicle Systems International, Baltimore, MD, June 1997.
C. Seibel, J.M. Farines, L. C. Correa, and G. C. Dallagnolo. Generating executable flight plans for unmanned aircraft: A formal mission planning tool. In Proceedings of the 13th Bristol International Conference on RPVs/UAVs, Bristol, UK, March 1998.
J. Unitt. A bright future for RPVs after Vietnam? Unmanned Systems, 11(2), 1993.
S. Yovine. Méthodes et Outils pour la Vérification Symbolique de Systèmes Temporisés. PhD thesis, Institut National Polytechnique de Grenoble, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seibel, C.W., Farines, JM., Cury, J.E.R. (1999). Towards Using Hybrid Automata for the Mission Planning of Unmanned Aerial Vehicles. In: Antsaklis, P., Lemmon, M., Kohn, W., Nerode, A., Sastry, S. (eds) Hybrid Systems V. HS 1997. Lecture Notes in Computer Science, vol 1567. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49163-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-49163-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65643-2
Online ISBN: 978-3-540-49163-7
eBook Packages: Springer Book Archive