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

  • Martin E. KüglerEmail author
  • Julian Rhein
  • Florian Holzapfel
Original Paper


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.


Model-based safety assessment Model checking Software validation Automatic landing Flight control Unmanned aerial vehicle 

List of symbols

\(CS\), \(MCS\)

Cut-sets, minimal cut-sets


Fault-activation inputs to model \({\mathcal{M}^*}\)

\(h\), \({h_{\text{meas}}}\)

Altitude, measurement thereof

\(\dot h,\;{\dot h_{\text{meas}}}\)

Vertical speed, measurement thereof

\({h_{\text{agl}}}\), \({h_{\text{RadAlt}}}\)

Height above ground level, radar altimeter measurement thereof

\(\mathcal{M}\), \({\mathcal{M}^*}\)

Software design model, with injected faults


Cut-set cardinality


Formalized property (i.e., requirement)

\(T\), \(F\)

True, false (logical)


Regular inputs to model \(\mathcal{M}\)


Weight on wheels status (logical)

\({{\Delta }}{h_{{\text{meas}},{\text{Bias}}}}\)

Bias of altitude measurement \({h_{\text{meas}}}\)

\({{\Delta }}{h_{F,{\text{Bias}}}}\)

Bias of flare altitude difference \({{\Delta }}{h_{F,{\text{nominal}}}}\)

\({{\Delta }}{h_{F,{\text{nominal}}}}\)

Altitude difference between start and end of flare in nominal automatic landing maneuver







Final descent




Reference point of the vehicle



Automatic take-off and landing


Computational tree logic


MBSA framework Exclude Cut-Sets


Flight control computer


Model-based safety assessment


Simulink Design Verifier


Unmanned aerial vehicle



The part of the work on MBSA techniques for software validation has been funded by the German Federal Ministry of Economics and Technology under the ZIM program (ZF 4037203BZ5). The SAGITTA research project was co-funded by Airbus Defence and Space in Manching, Germany and the project partners. The authors would like to thank Luca Evangelisti who contributed to the work in the scope of his graduation project, which he conducted very successfully under the supervision of the authors.


  1. 1.
    Brockhaus, R., Alles, W., Luckner, R.: Flugregelung [in German]. Springer, Berlin, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    SAE International: Guidelines for Development of Civil Aircraft and Systems, SAE ARP 4754A. Warrendale, PA (2010).
  3. 3.
    SAE International: Guidelines and methods for conducting the safety assessment process on civil airborne systems. SAE ARP 4761. Warrendale, PA (1996). Google Scholar
  4. 4.
    RTCA Inc.: Software considerations in airborne systems and equipment certification, RTCA DO-178C. Washington, D.C. (2011)Google Scholar
  5. 5.
    RTCA Inc.: Model-based Development and Verification Supplement to DO-178C and DO-278A, RTCA DO-331. Washington, D.C. (2011)Google Scholar
  6. 6.
    Amundson, I., Shipton, L.A., Liu, A., Nowak, M.: Toward efficient model-based development of aerospace applications. In: 15th AIAA Aviation Technology, Integration, and Operations Conference, AIAA AVIATION Forum (2015). Google Scholar
  7. 7.
    Walde, G., Luckner, R.: Bridging the tool gap for model-based design from flight control function design in simulink to software design in SCADE. In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), pp. 1-10 (2016). Google Scholar
  8. 8.
    Hochstrasser, M., Schatz S.P., Nürnberger K., Hornauer M., Myschik S., Holzapfel F.: Aspects of a consistent modeling environment for DO-331 design model development of flight control algorithms. In: Dołęga, B., Głębocki, R., Kordos, D., Żugaj, M. (eds) Advances in Aerospace Guidance, Navigation and Control. Springer, Cham (2017).
  9. 9.
    Lisagor, O., Kelly, T., Nui, R.: Model-based safety assessment: review of the discipline and its challenges. In: The Proceedings of 2011 9th International Conference on Reliability, Maintainability and Safety, pp. 625–632 (2011). Google Scholar
  10. 10.
    Bernard, R., Aubert, J.-J., Bieber, P., Merlini, C., Metge, S.: Experiments in model based safety analysis: flight controls. In: IFAC Workshop on Dependable Control of Discrete Systems, IFAC Proceedings 40(6), 43–48 (2007). Google Scholar
  11. 11.
    European Aviation Safety Agency (EASA): A harmonised European approach to a performance-based environment (PBE). [Online]. Cologne, Germany (2016). Accessed 08 Apr 2018
  12. 12.
    European Aviation Safety Agency (EASA): Introduction of a regulatory framework for the operation of unmanned aircraft systems in the ‘open’ and ‘specific’ categories, Opinion no. 01/2018. [Online]. Cologne, Germany (2018). Accessed 08 Apr 2018
  13. 13.
    Braun, S., Geiser, M., Heller, M., Holzapfel, F.: Configuration assessment and preliminary control law design for a novel diamond-shaped UAV. In: 2014 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 1009–1020 (2014). Google Scholar
  14. 14.
    Krause, C., Holzapfel, F.: Designing a System Automation for a novel UAV demonstrator. In: 2016 14th International Conference on Control, Automation, Robotics and Vision (ICARCV), pp. 1–6 (2016).
  15. 15.
    Kügler, M. E., Holzapfel, F.: Autoland for a Novel UAV as a State-Machine-based Extension to a Modular Automatic Flight Guidance and Control System. In: 2017 American Control Conference (ACC), pp. 2231–2236 (2017).
  16. 16.
    Kügler, M.E., Heller, M., Holzapfel, F.: Automatic take-off and landing on the maiden flight of a novel fixed-wing UAV. In: 2018 Flight Testing Conference, AIAA AVIATION Forum (2018). Google Scholar
  17. 17.
    Rees, M.: Airbus Jet-Propelled UAV demonstrator completes first test flight. [Online]. (2017). Accessed 08 Apr 2018
  18. 18.
    Kügler, M.E., Holzapfel, F.: Developing automated contingency procedures for the ATOL system of a fixed-wing UAV through online FDD. In: AIAA Modeling and Simulation Technologies Conference, AIAA AVIATION Forum (2016). Google Scholar
  19. 19.
    Arnold, A., Point, G., Griffault, A., Rauzy, A.: The AltaRica formalism for describing concurrent systems. Journal Fundamenta Informaticae 40(2–3), 109–124 (1999)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Rauzy, A.: Mode automata and their compilation into fault trees. Reliability Engineering and System Safety 78(1), 1–12 (2002). MathSciNetCrossRefGoogle Scholar
  21. 21.
    Bieber, P., Castel, C., Seguin, C.: Combination of fault tree analysis and model checking for safety assessment of complex system. In: Bondavalli, A., Thevenod-Fosse, P. (eds) Dependable Computing EDCC-4. EDCC 2002. Lecture Notes in Computer Science, vol 2485. Springer, Berlin, Heidelberg, pp. 19–31 (2002). Scholar
  22. 22.
    Bieber, P., Bougnol, C., Castel C., Heckmann, J.-P., Kehren, C., Metge, S., Seguin, C.: Safety assessment with Altarica—lessons learnt based on two aircraft system studies. In: Jacquart, R. (ed) Building the Information Society. IFIP International Federation for Information Processing, vol 156. Springer, Boston, MA (2004). Google Scholar
  23. 23.
    Kehren, C., Seguin, C., Bieber, P., Castel, C., Bougnol, C., Heckmann, J.-P., Metge, S.: Advanced simulation capabilities for Multi-systems with Altarica. In: Proceedings of the 22nd International System Safety Conference (ISSC), System Safety Society, pp. 489–498 (2004)Google Scholar
  24. 24.
    Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: the FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2003. Lecture Notes in Computer Science, vol 2788. Springer, Berlin, Heidelberg (2003). Google Scholar
  25. 25.
    Bozzano, M., Villafiorita, A., Akerlund, O., Bieber, P., Bougnol, C., Böde, E., Bretschneider, M., Cavallo, A., Castel, C., Cifaldi, M., Cimatti, A., Griffault, A., Kehren, C., Lawrence, B., Lüdtke, A., Metge, S., Papdopoulos, C., Passarello, R., Peikenkamp, T., Persson, P., Seguin, C., Trotta, L., Valacca, L., Zacco, G.: ESACS: an integrated methodology for design and safety analysis of complex systems. In: Bedford, T., van Gelder, P.H.A.J.M. (eds) Safety and Reliability: Proceedings of the ESREL 2003 Conference. Swets & Zeitlinger, Lisse, pp. 237–245 (2003).Google Scholar
  26. 26.
    Papadopoulos, Y., McDermid, J.A.: Hierarchically performed hazard origin and propagation studies. In: Felici, M., Kanoun, K. (eds) Computer Safety, Reliability and Security. SAFECOMP 1999. Lecture Notes in Computer Science, vol 1698. Springer, Berlin, Heidelberg (1999). Google Scholar
  27. 27.
    Papadopoulos, Y., Maruhn, M.: Model-based synthesis of fault trees from Matlab-Simulink models. In: 2001 International Conference on Dependable Systems and Networks, pp. 77–82 (2001).
  28. 28.
    Billings, C.E.: Aviation Automation: The Search for a Human-Centered Approach. Lawrence Erlbaum Associates, Mahwah (1997)Google Scholar
  29. 29.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  30. 30.
    Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1997. Lecture Notes in Computer Science, vol 1346. Springer, Berlin, Heidelberg (1997). Google Scholar
  31. 31.
    Monin, J.F., Hinchey, M.G.: Understanding formal methods. Springer, London (2003)CrossRefGoogle Scholar
  32. 32.
    Rozier, K.Y.: Linear Temporal Logic Symbolic Model Checking. Computer Science Review 5(2), 163–203 (2003). MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Biere, A., Cimatti, A., Clarke, E. M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg (1999). Google Scholar
  34. 34.
    Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham (2014). Google Scholar
  35. 35.
    The MathWorks Inc.: Simulink Design Verifier User’s Guide. [Online]. (2016). Accessed 27 Aug 2017
  36. 36.
    The MathWorks Inc.: Simulink Design Verifier Reference. [Online]. (2016). Accessed 27 Aug 2017
  37. 37.
    Kullaa, J.: Detection, identification, and quantification of sensor faults. In: Proceedings of the ISMA 2010 including USD 2010, pp. 893–907 (2010)Google Scholar
  38. 38.
    Vesely, W. E., Goldberg, F. F., Roberts, N. H., Haasl, D. F.: Fault tree handbook (NUREG-0492). US Nuclear Regulatory Commission, Washington, D.C., pp. VII–15ff (1981)Google Scholar

Copyright information

© Deutsches Zentrum für Luft- und Raumfahrt e.V. 2019

Authors and Affiliations

  1. 1.Institute of Flight System DynamicsTechnical University of MunichGarching Bei MünchenGermany

Personalised recommendations