{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/38920"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/38920","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Proving safety properties of an aircraft landing protocol using timed and untimed I/O automata : a case study","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Umeno, Shinya"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Nancy A. Lynch."],"committee_chairs":[],"committee_members":[],"year":2007,"date_issued":"2007","date_published":"2007","updated_at":"2026-07-22T22:20:47Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"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."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/38920","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Nancy A. Lynch."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Umeno, Shinya"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2007-09-28T13:08:09Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2007-09-28T13:08:09Z"]},{"key":"dc:date.issued","label":"Date","values":["2007"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/38920"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.","Page 222 blank.","Includes bibliographical references (p. 195-196)."]},{"key":"dc:description.abstract","label":"Abstract","values":["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.","(cont.) Using this new refinement, we carry over the verification results for the discrete model to the new model, and thus guarantee that the safe separation of aircraft verified for the discrete model also holds for the new model. We also prove properties specific to the new model, such as a lower bound on the spacing of aircraft in a specific area of the airport, using an invariant-proof technique."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["Proving safety properties of an aircraft landing protocol using timed and untimed I/O automata : a case study"]}]}],"canonical_facts":{"dc:contributor.advisor":["Nancy A. Lynch."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:creator":["Umeno, Shinya"],"dc:date.accessioned":["2007-09-28T13:08:09Z"],"dc:date.available":["2007-09-28T13:08:09Z"],"dc:date.issued":["2007"],"dc:description":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.","Page 222 blank.","Includes bibliographical references (p. 195-196)."],"dc:description.abstract":["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.","(cont.) Using this new refinement, we carry over the verification results for the discrete model to the new model, and thus guarantee that the safe separation of aircraft verified for the discrete model also holds for the new model. We also prove properties specific to the new model, such as a lower bound on the spacing of aircraft in a specific area of the airport, using an invariant-proof technique."],"dc:description.degree":["S.M."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/38920"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"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."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Proving safety properties of an aircraft landing protocol using timed and untimed I/O automata : a case study"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:20:47Z"}