Abstract
The air traffic management system is under generalized upgrading process. New requirements of safety arise based on several emerging technologies. This work presents a model to automatically verify safety of actions taken by human traffic controllers in frequent situations. The model uses the formalism of hybrid automata, and consists basically on segmenting the space of routes and associating each segment to a location of the automaton. Some kind of trajectory optimisation is also possible with this model.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bonifácio, A. L.: Verificação e Síntese de Sistemas Híbridos, MSc. Dissertation, Instituto de Computação Unicamp, 2000.
Tomlin, C.; Lygeros, J.; Sastry, S.: Synthesizing Controllers for Non-linear Hybrid Systems. LNCS 1386, Springer-Verlag, 1998.
Tomlin, C.; Lygeros, J.; Sastry S.: Computing Controllers for Non-linear Hybrid Systems. LNCS 1569, Springer-Verlag, 1999.
GodHavn, J. M.; Lauvdal, T.; Egeland, O.: Hybrid Control in Sea Traffic Management Systems. LNCS 1066, Springer-Verlag, 1996.
Lygeros, J.; Lynch, N. A: Strings of Vehicles: Modelling and Safety Conditions. LNCS 1386, Springer-Verlag, 1998.
Lynch, N.: High-Level Modelling and analysis of an Air-Traffic Management System. LNCS 1569, Springer-Verlag, 1999.
Lygeros, J., Pappas, G. J.; Sastry, S.: An Approach to the Verification of the-TRACON Automation System. LNCS, Springer-Verlag, 1998.
Egerstedt, M., Koo, T. J., Hoffmann, F., Sastry, S.: Path Planning and Flight Controller Scheduling for an Autonomous Helicopter. LNCS 1569, Springer-Verlag, 1999.
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: 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, Lecture Notes in Computer Science 736, pages 209–229. Springer-Verlag, 1993.
Alur, R., Henzinger, T.A., Ho, P.-H. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993. Full version appears in IEEE Transactions on Software Engineering, 22(3): 181-201, 1996.
Henzinger, T. A., Ho, P.-H., Wong-Toi, H.: HyTech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 56–65. IEEE Computer Society Press, 1995.
Henzinger, T. A., Ho, P.-H., Wong-Toi, H.: A user guide to HyTech. In E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Steen, editors, TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1019, pages 41–71. Springer-Verlag, 1995.
Henzinger, T. A., Nicollin, X., Sifakis, J., and Yovine, S. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
Henzinger, T. A., Wong-Toi, H.: Linear phase-portrait approximations for non-linear hybrid systems. In R. Alur and T.A. Henzinger, editors, Hybrid Systems III, Lecture Notes in Computer Science. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Oliveira, Í.R., Cugnasca, P.S. (2002). Checking Safe Trajectories of Aircraft Using Hybrid Automata. In: Anderson, S., Felici, M., Bologna, S. (eds) Computer Safety, Reliability and Security. SAFECOMP 2002. Lecture Notes in Computer Science, vol 2434. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45732-1_22
Download citation
DOI: https://doi.org/10.1007/3-540-45732-1_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44157-1
Online ISBN: 978-3-540-45732-9
eBook Packages: Springer Book Archive