Validation of decision logic of an autoland system for a UAV using model-based safety-assessment techniques

Software of automatic flight control systems requires thorough verification and validation. Traditionally, this is achieved with elaborate development processes following pertinent industry standards. To reduce the development effort, however, new methods have emerged: a model-based software development process is used at the Institute of Flight System Dynamics of the Technical University of Munich for the design of auto-flight systems with MATLAB/Simulink. Besides, the model-based safety assessment (MBSA) framework ExCuSe has been developed, which implements methods for fault modeling and automatic cut-set extraction using the Simulink Design Verifier. This paper proposes an application of MBSA techniques for the efficient requirements and design validation of decision logic in auto-flight-system software. With ExCuSe, software design models of an investigated decision logic are supplemented by models for off-nominal inputs (e.g., a sensor fault) and for the design requirements. With the analysis, either a formal proof is obtained that the investigated decision logic fulfills the requirements under any circumstances (guaranteed properties), or a counterexample illustrates a requirement violation. The functional principle and applicability of the method are demonstrated by the analysis of decision logic of the autoland system of the SAGITTA Demonstrator UAV. ExCuSe is used to prove that the logic guarantees a timely flare initiation so that a safe touchdown sink rate is achieved despite altitude-measurement inaccuracy and closed-loop flare dynamics uncertainty. As virtually all auto-flight systems feature decision logic, this initial demonstration of the technique opens up many opportunities for further applications in future work.