Investigation and Automation of Verification Methods for Model-Based Development of GNC Systems

Kurzfassung

Objective: The presented work considers the development of guidance, navigation and control (GNC) software in the context of reusable launch vehicles. More specifically, the considered workflows involve modeling in Matlab/Simulink and automated code generation with the goal of deployment to real-time embedded system processors. The objective is to investigate, evaluate and automate the use of several compatible software verification tools at different points of this process. Methods: An example project is developed to resemble the software that is developed in a project context. The considered tools are introduced and investigated in that context for their usability and limitations. Both static and dynamic verification are considered, taking current formal methods into account. Methods for static analysis of Matlab code, Simulink models and generated code are presented as well as an alternative method of testing in Simulink. Results: The work results in a review of the tools capabilities and limitations. A basic framework of wrapper functions to use the tools is developed in the process. This encompasses an automation concept for the use in GitLab with an automated evaluation of verification results. Lastly, an initial qualitative evaluation of the tools is provided. Conclusion: The presented suite of tools is able to significantly increase the level of confidence in software quality, when it is used correctly. This means that they require to be used in conjunction within a well-defined process and respecting their individual limitations. Concluding, recommendations for next steps and a prioritization for implementation in a project context are given.