| 军工高安全软件数值型运行时错误分析方法 |
| |
| 引用本文： | 黄明,詹海潭,张伟,经小川,李宁,王潇茵.军工高安全软件数值型运行时错误分析方法[J].空间控制技术与应用,2016,42(6):58-62. |
| |
| 作者姓名： | 黄明 詹海潭 张伟 经小川 李宁 王潇茵 |
| |
| 作者单位： | 中国工程物理研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院 |
| |
| 基金项目： | 国家自然科学基金资助项目（91418204） |
| |
| 摘 要： | 提出一种抽象解释和有界模型验证的数值型运行时错误分析方法.利用抽象解释方法分析程序数值变量范围，获得每个程序点达到不动点的变量初步值范围信息.根据待分析的运行时错误类型，在相关需要检测的程序点处将数值变量取值信息转化为断言或假设形式插入程序中，将带有断言和假设的程序转化为布尔公式，验证其可满足性，进而验证断言的正确性.实验证明，该方法与现有方法相比，在精度和效率两方面都有良好的表现.
|
| 关 键 词： | 抽象解释 有界模型验证 数值型运行时错误 值范围分析 |
Numerical Runtime Error Check of Aerospace Safety Critical Software |
| |
| HUANG Ming,ZHAN Haitan,ZHANG Wei,JING Xiaochuan,Li Ning and Wang Xiaoyin.Numerical Runtime Error Check of Aerospace Safety Critical Software[J].Aerospace Contrd and Application,2016,42(6):58-62. |
| |
| Authors: | HUANG Ming ZHAN Haitan ZHANG Wei JING Xiaochuan Li Ning and Wang Xiaoyin |
| |
| Institution: | China Academy of Engineering Physics, Mianyang 621900, China;China Academy of Aerospace Systems Science and Engineering, Beijing 100048, China;China Academy of Aerospace Systems Science and Engineering, Beijing 100048, China;China Academy of Aerospace Systems Science and Engineering, Beijing 100048, China;China Academy of Aerospace Systems Science and Engineering, Beijing 100048, China;China Academy of Aerospace Systems Science and Engineering, Beijing 100048, China |
| |
| Abstract: | |
| |
| Keywords: | abstract interpretation bounded model check numerical runtime error value analysis |
|
| 点击此处可从《空间控制技术与应用》浏览原始摘要信息 |
| 点击此处可从《空间控制技术与应用》下载免费的PDF全文 |
|
