Institutional Repository
| Formal verification of a descent guidance control program of a lunar lander | |
| Zhao, Hengjun (1); Yang, Mengfei (2); Zhan, Naijun (1); Gu, Bin (3); Zou, Liang (1); Chen, Yao (3); Zhan, N.(znj@ios.ac.cn) | |
| 2014 | |
| Conference Name | 19th International Symposium on Formal Methods, FM 2014 |
| Pages | 733-748 |
| Conference Date | May 12, 2014 - May 16, 2014 |
| Conference Place | Singapore, Singapore |
| Indexed Type | CPCI ; EI |
| Publish Place | Springer Verlag |
| ISSN | 3029743 |
| ISBN | 9783319064093 |
| Department | (1) State Key Lab. of Computer Science, Institute of Software, CAS, Beijing, China; (2) Chinese Academy of Space Technology, Beijing, China; (3) Beijing Institute of Control Engineering, Beijing, China; (4) University of Chinese Academy of Sciences, Beijing, China |
| English 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 techniques including simulation, bounded model checking (BMC) and theorem proving, 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 verification, trustworthiness of the lunar lander's control program is enhanced. © 2014 Springer International Publishing Switzerland.; 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 techniques including simulation, bounded model checking (BMC) and theorem proving, 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 verification, trustworthiness of the lunar lander's control program is enhanced. © 2014 Springer International Publishing Switzerland. |
| Keyword | Lunar Lander Formal Verification Hybrid Systems Reachable Set Invariant |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16511 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Zhan, N.(znj@ios.ac.cn) |
| Recommended Citation GB/T 7714 | Zhao, Hengjun ,Yang, Mengfei ,Zhan, Naijun ,et al. Formal verification of a descent guidance control program of a lunar lander[C]. Springer Verlag,2014:733-748. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment