APP下载

基于KeY的程序分析和验证

2016-05-16夏新凯陈冬火

软件 2016年3期
关键词:可信性规约软件测试

夏新凯+陈冬火

摘要:可信性是各安全攸关领域软件的基础要求,例如航空航天飞行器控制软件、核电站控制软件和交通控制管理软件等,基于形式化方法的程序验证和分析是确保软件正确,具有可信性的重要手段。相比软件测试,基于定理证明的程序验证具有语法和语义的严格性,和属性相关的完备性。本文对程序形式化Hoare语义规约和相关的程序逻辑推理规则系统进行了详细的讨论。基于形式化验证平台KeY,采用完全自动化和交互式两种方法,对具有一定规模的,含有循环结构,并且具有实际意义的程序进行验证。研究证明过程的具体证明策略和方法,尤其是关于循环不变式的规约方法;对KeY的证明效率,先进性和局限性进行评估。endprint

猜你喜欢

可信性规约软件测试
可变情报板发布内容可信性检测系统探究
基于可信性的锅炉安全质量综合评价研究
基于OBE的软件测试课程教学改革探索
在区间上取值的模糊变量的可信性分布
电力系统通信规约库抽象设计与实现
一种在复杂环境中支持容错的高性能规约框架
EXCEL和VBA实现软件测试记录管理
Five golden rules for meeting management
关于软件测试技术应用与发展趋势研究
一种改进的LLL模糊度规约算法