基于语境的ARINC653操作系统核心服务正确性形式证明方法

摘要

随着安全关键软件规模的不断增长、复杂性的持续扩大,其形式验证难度也越来越高.传统的形式验证方法如Floyd提出的"断言式方法"、Hoare提出的"公理式方法",存在断言构造依赖于操作人员的实际工作能力、循环不变式生成复杂、证明复杂度高等不足之处.本文在Hoare逻辑核心特性的Hoare三元组的基础上,提出基于语境的程序正确性形式证明方法:用语境来记录程序运行的上下文;将高层需求抽象为功能模型,并将其描述为前后置条件形式;将高层需求前置条件作为待证明程序的初始语境,经过待证明程序执行到达终止语境,程序正确性形式证明即为验证终止语境与高层需求后置条件的一致性.本文以形式证明ARINC653操作系统核心服务建模程序正确性为目标,为此,首先对ARINC653操作系统57个核心服务进行建模并将高层需求描述为前后置条件形式;之后构造一套将程序语句转化为逻辑语句的形式公理系统,将核心服务模型转化为逻辑语句序列以待证明;最后开发出一个基于语境的程序正确性形式证明工具,将上述逻辑语句序列和高层需求前置条件作为输入,经过一系列语境代入合并操作以及终止语境与高层需求后置条件匹配操作,从而得到ARINC653操作系统核心服务正确性证明结果.本文设计的基于语境的程序正确性形式证明方法能够简化验证的难度,提高证明的自动化程度.