Proving safety properties of an aircraft landing protocol using timed and untimed I/O automata : a case study

This thesis presents an assertional-style verification of the aircraft landing protocol of NASA's SATS (Small Aircraft Transportation System) concept of operation using the timed and untimed I/O automata frameworks. We construct two mathematical models of the landing protocol using the above stated frameworks. First, we study a discrete model of the protocol, in which the airspace of the airport and every movement of the aircraft are all discretized. The model is constructed by reconstructing a mathematical model presented in using the untimed I/O automata framework. Using this model, we verify the safe separation of aircraft in terms of the bounds on the numbers of aircraft in specific discretized areas. In addition, we translate this I/O automaton model into a corresponding PVS specification, and conduct a machine verification of the proof using the PVS theorem prover. Second, we construct a continuous model of the protocol by extending the discrete model using the timed I/O automata framework. A refinement technique has been developed to reason about the external behavior between two systems. We present a new refinement proof technique, a weak refinement using a step invariant.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2007

Author dc:creator

• Umeno, Shinya

Advisor dc:contributor.advisor

• Nancy A. Lynch.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/38920

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/38920