Timely flare initiation during automatic landing – A model checking application example

In an automatic landing maneuver, it is crucial that the automatic flight system which controls the aircraft initiates the flare in the right moment. Especially a too late flare initiation is critical, as it could result in a hard touchdown. Typically, a decision logic of the automatic flight system evaluates an altitude measurement for the initiation of the flare. The verification and validation of such systems is traditionally accomplished with Monte-Carlo simulation analysis and possibly additional flight tests. At the Institute of Flight System Dynamics of the Technical University of Munich, an automatic landing system has been developed and flight tested on the maiden flight of the advanced unmanned aircraft ‘SAGITTA Demonstrator.’ In addition to traditional simulation testing, the flare decision logic of the system has been used as an application example for verification and validation with model checking methods, using the Simulink Design Verifier by The MathWorks Inc. With it, it could be formally proven that the formulated decision logic ensures a touchdown with an adequate sink rate when the relevant uncertainties can be confined to values obtained in the analysis. In comparison to Monte-Carlo methods, this result was obtained at significantly lower computational cost and represents a formal proof in contrast to statistical distributions.