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) |
| 出版日期 | 2014 |
| 会议名称 | 19th International Symposium on Formal Methods, FM 2014 |
| 会议日期 | May 12, 2014 - May 16, 2014 |
| 会议地点 | Singapore, Singapore |
| 关键词 | Lunar lander formal verification hybrid systems reachable set invariant |
| 页码 | 733-748 |
| 通讯作者 | Zhan, N.(znj@ios.ac.cn) |
| 中文摘要 | 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. |
| 收录类别 | CPCI ; EI |
| 会议录出版地 | Springer Verlag |
| 语种 | 英语 |
| ISSN号 | 3029743 |
| ISBN号 | 9783319064093 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16511]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Zhao, Hengjun ,Yang, Mengfei ,Zhan, Naijun ,et al. Formal verification of a descent guidance control program of a lunar lander[C]. 见:19th International Symposium on Formal Methods, FM 2014. Singapore, Singapore. May 12, 2014 - May 16, 2014. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。