Research Abstracts - 2006

Proving Safety Properties of an Aircraft Landing Protocol using Timed/untimed I/O Automata

S. Umeno & N. Lynch

Introduction

Continuing from the last year, we will study the landing protocol of the NASA's SATS concept of operations[1], as a case study of the application of timed/untimed I/O automata framework [4,5]. The SATS program aims to increase access to small and medium sized airports. The situation is significantly different in these airports from large airports, where separation assurance services are provided by the Air Traffic Control (ATC). Due to the limited facilities and inferior infrastructure in such airports, in the SATS concept, a centralized air traffic management system is automated and does its minimal job to achieve the safety landing of the aircraft. It is the pilots' responsibility to determine the moment when their aircraft initiate the final approach initiation to the ground. Pilots follow the procedures defined in the SATS concept of operation to control their aircraft in a designated area in the air space of the airport, called the Self Controlled Area. It is crucial to guarantee a safe separation of the aircraft in the Self Controlled Area, provided that each pilot follows the procedures of the SATS concept. For this reason, a mathematical model of the SATS concept of operations is presented in [2] and [3], and some properties of the model that represent the safety separation of the aircraft have been exhaustively checked using a model-checking technique. Our objectives are: first, constructing a more standardized and comprehensive representation of the model using the timed/untimed I/O automata framework; and second, carrying out the proof of the safety properties of the constructed model using the proof techniques for the framework, such as the invariant proof technique, and the refinement.

Approach

We use the timed/untimed I/O automata framework to model the landing protocol. The untimed I/O automata have been successfully used to model nondeterministic distributed systems and to prove properties of them. Their treatment of nondeterminism is suitable for reconstructing the discrete model presented in [2] in which the next possible step that the model can take is nondeterministically defined. The timed I/O automata has been developed for modeling the system with both the continuous and timed dynamics and the discrete transitions of the states. We will use this framework to construct the continuous model of the protocol. The continuous model we will construct is intended to capture the dynamics of the aircraft and the geometry of the airport with a finer granularity than the discrete model so that we can examine the properties that involves a finer geometric and aircraft-dynamics consideration.

Progress

We first reconstructed the discrete version of the model presented in [2] using I/O automata, in which the airspace of the airport and every movement of the aircraft are all discretized. Though the protocol is complex, the IOA code we constructed has a manageable form, and is more comprehensible than the original presentation of the model in [2]. We finished proving interesting safety properties of the model proposed in [2]. These properties include the invariants of the model that state that no more than four aircraft are in the entire Self Controlled Area, or there is at most one aircraft at a certain part of the airspace in the airport. We also have rigorously checked all the proofs using the PVS mechanical theorem prover [6]. We found that using a mechanical prover is very helpful in managing a large proof for a moderately complex system such as ours.

Work in progress

We are planning to construct the continuous model of the landing protocol using timed I/O automata. We succeeded to verify the safety separation of aircraft in terms of the bound on the number of aircraft in the specific discretized area. However, to examine properties that involve more realistic dynamics of aircraft, such as the spacing between aircraft, we need a more precise modeling of the aircraft kinematics and the geometry of the airport. A continuous model, such as the one presented in [3], is suitable to deal with such properties. In [3], only the dynamics of aircraft in some specific portion of the airspace in the airport is modeled as a continuous behavior of the model, and the rest of the airspace remain to be discretized. In other words, the continuous version of that specific area, along with the associated movement of aircraft, is ``embedded'' into the original discrete model. We intend to capture more dynamics of aircraft in our new continuous model than the model in [3] does, by not just focusing on the specific area, but also expressing the rest of the areas with some continuous feature. We will construct the new model so that we can consider it as an extended version of the discrete model. This can be done by partitioning the air space of the airport based on the discretized zones in the discrete model, and by having the discrete transitions corresponding to the original transitions, as well as the continuous behavior expressed as a notion called ``trajectories'' in the timed I/O automata framework. Using the mathematical verification techniques for timed I/O automata, we will also explore if the results in this work can carry over to the new model.

Research Support

This research is supported by Air Force Contract FA9550-04-C-0084.

References

[1] T.Abbott, K. Jones, M. Consiglio, D. Williams, and C. Adams Small Aircraft Transportation System, High Volume Operation concept: Normal operations. Technical Report NASA/TM-2004-213022, NASA Langley Research Center, NASA LaRC,Hampton VA 23681-2199, USA, March, 2004.

[2] G. Dowek, C. Munoz, and V. Carreno. 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 VA 23681-2199, USA, March 2004.

[3] C. Mu~noz and G. Dowek. Hybrid verication of an air trac operational concept. In Proceedings of IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verication, and Validation, Columbia, Maryland, 2005.

[4] Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996.

[5] Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. The theory of timed I/O automata. Technical Report MIT-LCS-TR-917a, MIT Laboratory for Computer Science, Cambridge, MA, USA, November 2004.

[6] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verication system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Computer Science, pages 748-752, Saratoga, NY, June 1992.