Y.: Formal verification of a descent guidance control program of a lunar

Abstract. We report on our recent experience in applying formal methods to the verification of a descent guidance control program of a lunar lander. The powered descent process of the lander gives a specific hybrid system (HS), i.e. a sampled-data control system composed of the physical plant and the embedded control program. Due to its high complexity, verification of such a system is very hard. In the paper, we show how this problem can be solved by several different tech-niques including simulation, bounded model checking (BMC) and theorem prov-ing, using the tools Simulink/Stateflow, iSAT-ODE and Flow∗, and HHL Prover, respectively. In particular, for the theorem-proving approach to work, we study the invariant generation problem for HSs with general elementary functions. As a preliminary attempt, we perform verification by focusing on one of the 6 phases, i.e. the slow descent phase, of the powered descent process. Through such verifi-cation, trustworthiness of the lunar lander’s control program is enhanced