General aviation landing assistance using formal methods-based system design

This paper presents the use of a formal methods-based system design methodology in order to develop a general aviation landing assistance system that is safe by design. Therefore the aircrafts aerodynamic characteristics integrated in a simplified physical model as well as the operational modes during the landing maneuver are integrated into a hybrid system. Such a hybrid system represents both discrete and continuous state dynamics and it can be used to perform reachability analysis. These analyses shall identify invariant sets which represent the safe flight envelope for a certain phase during the landing approach. In this simplified model the operational modes that have to be investigated are Flare, Rollout, Altitude, and Takeoff/Go-Around in case of a missed approach. The resulting invariant sets shall represent all states that allow the aircraft to land safely within a certain target set. Furthermore it shall be calculated whether a recovery maneuver can be safely initiated or not in case of a missed approach. Based on these calculations a discrete system representation shall be used to design a user interface prototype that covers all operational modes as well as the physical capabilities of the aircraft. The benefit of such a user interface shall be an increased situational awareness as well as the reduction of dangerous phenomena like mode confusion.