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

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