Combining Formal and Informal Methods in the Design of Spacecrafts

摘要

In this chapter, we summarize our experience on combing formal and informal methods together in the design of spacecrafts. With our approach, the designer can either build an executable model of a spacecraft using the industrial standard environment Simulink/Stateflow, which facilitates analysis by simulation, or construct a formal model using Hybrid CSP (HCSP), which is an extension of CSP for formally modeling hybrid systems. HCSP processes can be specified and reasoned about by Hybrid Hoare Logic (HHL), which is an extension of Hoare logic to hybrid systems. The connection between informal and formal methods is realized via an automatic translator from Simulink/Stateflow diagrams to HCSP and an inverse translator from HCSP to Simulink. The advantages of combining formal and informal methods in the design of spacecrafts include 1. It enables formal verification as a complementation of simulation. As the inherent incompleteness of simulation, it has become an agreement in industry and academia to complement simulation with formal verification, but this issue still remains challenging although lots of attempts have been done (see the related work section); 2. It provides an option to start the design of a hybrid system with an HCSP formal model, and simulate and/or test it using Matlab platform economically, without expensive formal verification if not necessary; 3. The semantic preservation in shifting between formal and informal models is justified by co-simulation. Therefore, it provides the designer the flexibility using formal and informal methods according to the trade-off between efficiency and cost, and correctness and reliability. We will demonstrate the above approach by analysis and verification of the descent guidance control program of a lunar lander, which is a real-world industry example.