Sciweavers

Share
HYBRID
2007
Springer

Safety Verification of an Aircraft Landing Protocol: A Refinement Approach

9 years 7 months ago
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.
Shinya Umeno, Nancy A. Lynch
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where HYBRID
Authors Shinya Umeno, Nancy A. Lynch
Comments (0)
books