Abstract
In this paper, we propose a new approach for formal verification of hybrid systems. To do so, we present a new refinement proof technique, a weak refinement using step invariants. As a case study of the approach, we conduct formal verification of the safety properties of NASA’s Small Aircraft Transportation System (SATS) landing protocol. A new model is presented using the timed I/O automata (TIOA) framework [1], and key safety properties are verified. Using the new refinement technique presented in the paper, we first carry over the safety verification results from the previous discrete model studied in [2] to the new model. We also present properties specific to the new model, such as lower bounds on the spacing of aircraft in specific areas of the airspace.
This project is supported by Air Force Contract FA9550-04-C-0084.
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
Kaynar, D.K., et al.: The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science. Morgan & Claypool Publishers, San Rafael (2006)
Umeno, S., Lynch, N.: Proving safety properties of an aircraft landing protocol using I/O automata and the PVS theorem prover: a case study. In: Wimmer, M.A., et al. (eds.) EGOV 2006. LNCS, vol. 4084, pp. 64–80. Springer, Heidelberg (2006)
Steiner, W., et al.: Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation. In: Proc. of the 2004 International Conference on Dependable Systems and Networks, Florence, Italy, pp. 189–198. IEEE Computer Society Press, Los Alamitos (2004)
Kopetz, H., Bauer, G.: The time-triggered architecture. Proceedings of The IEEE 91, Part 1, 112–126 (2003)
Abbott, T.: Jones, K., Consiglio, M., Williams, D., Adams, C.: Small Aircraft Transportation System, High Volume Operation concept: Normal operations. Technical Report NASA/TM-2004-213022, NASA Langley Research Center, NASA LaRC, Hampton, USA (2004)
Dowek, G., Muñoz, C., Carreño, V.: Abstract model of the SATS concept of operations: Initial results and recommendations. Technical Report NASA/TM-2004-213006, NASA Langley Research Center, NASA LaRC, Hampton, USA (2004)
Muñoz, C., Dowek, G.: Hybrid verification of an air traffic operational concept. In: Proceedings of IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, Columbia, Maryland, IEEE Computer Society Press, Los Alamitos (2005)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Lynch, N., Segala, R., Vaandraager, F.: Hybrid I/O automata. Information and Computation 185(1), 105–157 (2003)
Mitra, S., et al.: Safety verification of model helicopter controller using hybrid Input/Output automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, Springer, Heidelberg (2003)
Livadas, C., Lygeros, J., Lynch, N.A.: High-Level Modeling and Analysis of the Traffic Alert and Collision Avoidance System (TCAS). Proceedings of the IEEE, Special Issue on Hybrid Systems: Theory & Applications 88(7), 926–948 (2000), http://theory.lcs.mit.edu/tds/papers/Livadas/IEEE00.html
Fehnker, A., Zhang, M., Vaandrager, F.W.: Modeling and verifying a lego car using hybrid I/O automata. In: Third International Conference on Quality Software (QSIC 2003), Dallas, Texas, USA, November 2003, IEEE Computer Society Press, Los Alamitos (2003)
Lynch, N., Vaandrager, F.: Forward and backward simulations – part II: Timing-based systems. Information and Computation 128(1), 1 (1996)
Umeno, S.: Proving safety properties of an aircraft landing protocol using timed and untimed I/O automata: a case study. Master’s thesis, Massachusetts Institute of Technology, Cambridge, MA (2006)
Henzinger, T.A., Minea, M., Prabhu, V.: Assume-guarantee reasoning for hierarchical hybrid systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 275–290. Springer, Heidelberg (2001)
Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction. In: CDC 2004: IEEE Conference on Decision and Control, IEEE Computer Society Press, Los Alamitos (2004)
Garland, S.: TIOA User Guide and Reference Manual (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Umeno, S., Lynch, N. (2007). Safety Verification of an Aircraft Landing Protocol: A Refinement Approach. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds) Hybrid Systems: Computation and Control. HSCC 2007. Lecture Notes in Computer Science, vol 4416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71493-4_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-71493-4_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71492-7
Online ISBN: 978-3-540-71493-4
eBook Packages: Computer ScienceComputer Science (R0)