Proceedings of the

The 33rd European Safety and Reliability Conference (ESREL 2023)
3 – 8 September 2023, Southampton, UK

A Formal Verification Framework for Model Checking Safety Requirements of a Simulink Landing Gear Case Study

Tim Gonschorek1,a, Hannes Stützer1,b, Frank Ortmeier1,c, Leon Wehmeier2 and Michael Oppermann3

1Faculty of Computer Science, Otto-von-Guericke-University Magdeburg, Germany.

2Department of Production and Wood Technology, OWL University of Applied Sciences and Arts, Germany.

3Aribus Operations GmbH, Germany.


The request for computer-aided system verification approaches increases with rising system complexity. So, integrating formal verification approaches, e.g., model checking, into the typical engineering workflow could help keep up with this rising complexity. Therefore, however, such an analysis of a system model must cover widely applied design specification languages, e.g., Matlab Simulink or Modelica.

This paper shall provide an approach for transforming a Simulink model into the input language of a model checking verification tool. Therefore, we modeled a widely applied case study of an aircraft landing gear system to provide a formal framework that can later be translated into a Kripke structure. A widely used formalism for verification tool input languages. The set of Matlab Simulink elements for which we provide a translation is derived from the model itself. To prove that the translation preserves the model's semantics, we also define a formal representation of the modeled Simulink elements. The translation enables us to apply several model checking tools for formal verification.

Keywords: Model-based safety assessment, Model checking, Integrated safety design.

Download PDF