Formal verification of a descent guidance control program of a lunar lander

ISCAS OpenIR

	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
会议名称	19th International Symposium on Formal Methods, FM 2014
页码	733-748
会议日期	May 12, 2014 - May 16, 2014
会议地点	Singapore, Singapore
收录类别	CPCI ; EI
出版地	Springer Verlag
ISSN	3029743
ISBN	9783319064093
部门归属	(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
摘要	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.
关键词	Lunar Lander Formal Verification Hybrid Systems Reachable Set Invariant
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16511
专题	中国科学院软件研究所
通讯作者	Zhan, N.(znj@ios.ac.cn)
推荐引用方式 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.