|
|||||
|
|
| 军工高安全软件数值型运行时错误分析方法 | |
| 作者姓名： | 黄明 詹海潭 张伟 经小川 李宁 王潇茵 |
| 作者单位： | 中国工程物理研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院;中国航天系统科学与工程研究院 |
| 基金项目： | 国家自然科学基金资助项目（91418204） |
| 摘 要： | 提出一种抽象解释和有界模型验证的数值型运行时错误分析方法.利用抽象解释方法分析程序数值变量范围,获得每个程序点达到不动点的变量初步值范围信息.根据待分析的运行时错误类型,在相关需要检测的程序点处将数值变量取值信息转化为断言或假设形式插入程序中,将带有断言和假设的程序转化为布尔公式,验证其可满足性,进而验证断言的正确性.实验证明,该方法与现有方法相比,在精度和效率两方面都有良好的表现. |
| 关 键 词： | 抽象解释 有界模型验证 数值型运行时错误 值范围分析 |
| 点击此处可从《空间控制技术与应用》浏览原始摘要信息 | |
| 点击此处可从《空间控制技术与应用》下载全文 | |