Introduction

As a new example of the TIOA project, we are now studying a model for the Small Aircraft Transportation System (SATS), a system for landing aircraft in small and medium airports currently being studied as a joint project of NASA and several universities. Our study on this model is based on the work of Cesar Munoz in National Institute of Aerospace (NIA), and his colleagues [1], on which a mathematical model for the system was presented. They modeled the system by discretizing the space of the airport into several zones represented as queues of aircraft, and under such a discrete system model, some interesting properties of the system are proved by a state exploration method using a mechanical theorem prover PVS. These properties include the bounds on the number of aircraft in a specific zone of the system and the number of simultaneous operations of the aircrafts.

Approach

One objective for us to conduct research on this model is to see if we can prove the properties presented on the paper by means of a standard invariant-proof technique using tools, techniques, and experiences we have used from earlier examples. We chose some properties from the original work and developed a revised PVS specification from the original model (revised so that it becomes more handy for invariant-style proofs, without the changes in the semantics.)

Progress

The difficulties are in having auxiliary lemmas to make the inductive proofs go through, as opposed to the state exploration method, which will explore the entire state spaces to directly check the properties. We developed such lemmas and now working on the proof of them in PVS.

Future

In addition to the discrete model, the original authors of the first model of the system are now trying to refine the model to treat a continual behavior of the system such as the movement of the aircraft or a space between aircrafts. We are communicating with them to see how this attempt can be accomplished in the TIOA framework. When we finish proving properties of the discrete model, we will move on to the study of a continuous model in collaboration with the original authors.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References

[1]: G. Dowek, C. Munoz, and V. Carreno. Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations. NASA Technical Memo NASA/TM-2004-213006, NASA Langley Research Center, Hampton, VA, March 2004.