Safety Verification of an Aircraft Landing Protocol: A Refinement Approach

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.

• Type: Conference
• Year: 2007
• Where: HYBRID
• Authors: Shinya Umeno, Nancy A. Lynch
• Keywords: Control Systems, Formal Verification, HYBRID 2007, Safety Properties, Small Aircraft Transportation System