Page 13 - 《软件学报》2021年第10期

高猛 等:航天嵌入式软件整数溢出的形式化验证方法 2985

操作将状态 s 5 上变量 x 赋值为 v 2 ,即:对于 W-W 模型中的共享数据单元 x,ISR i 对变量 x 的作用已被 P
中 WRITE 操作清除.

(a) R-R 模型 (b) W-R 模型 (c) R-W 模型 (d) W-W 模型
Fig.9 Model of an interrupt-driven program
图 9 中断驱动程序模型

对于程序 P 和中断 ISR i ,v 是 P 中语句 St 上的一个全局变量.基于对中断驱动程序模型的分析,我们能够得
出以下推论.
(1) 若 ISR i 不存在对 v 的写操作,则语句 St 的执行不受中断影响;
(2) 若 St 中存在对 v 的写操作且 ISR i 中存在对 v 的写操作,则语句 St 的执行不受中断影响;
(3) 若 St 中存在对 v 的读操作且 ISR i 中存在对 v 的写操作,则语句 St 的执行受中断影响.
2.3.2 基于函数摘要的中断函数特征分析
首先,基于上一节提出的中断驱动程序模型推论,给出干扰变量的定义.
定义 2(干扰变量). 对于程序 P 和中断向量号为 i 的中断 ISR i ,Vars(P)表示程序 P 上的全局变量集合,
Vars(ISR i )表示中断 ISR i 上的全局变量集合,assess(proc,t)表示变量 t 在程序 proc 上的访问方式,St 表示程序 P 上
的任意一个语句.v 是语句 St 上的一个全局变量,若满足以下两个条件:
(1) 变量 v 属于集合 Vars(P)且变量 v 属于集合 Vars(ISR i );
(2) assess(P,v)为读访问方式且 assess(ISR i ,v)为写访问方式,
st
则称变量 v 为中断 ISR i 对程序 P 上语句 St 的干扰变量,记为 v .其中,中断 ISR i 称为干扰中断.
由于在主程序执行过程中,中断 ISR i 可能在主程序的任何一个语句处发生;而且随着主程序循环的执行,中
断发生次数是不确定的;同时,中断 ISR i 的触发本质上也属于函数调用.因此,我们可以将中断函数 ISR i 理解为被
调用函数,记为函数 ISR i Proc,其形式可以描述为
j:=0; while (j<nondetnum()){ISR i ();j++},
其中,函数 nondetnum()随机返回 1 个正整数.
更一般地,在航天嵌入式软件中断设计中,不同中断完成各自相对独立的功能,其干扰变量集合各不相同,
st
st
因此我们可以将不同中断上的干扰变量分别单独考虑.在中断函数 ISR i 中,对于干扰变量 v 写访问,v 取值范围
st
st
不随中断发生次数的增加而改变;对于干扰变量 v 读写访问,v 的取值范围随着中断发生次数的增加而扩大,
st
在整数溢出有界模型检测验证时仅考虑 v 最大取值范围即可.因此,函数 ISR i Proc 可进一步描述为以下形式:
while (true){ISR i ();}.
对于中断驱动型程序的整数溢出检测,我们所关心的仅是中断函数调用对干扰变量的更新和修改.因此,本
文采用函数摘要机制将中断函数特征近似抽象为三元组VecNum,VarInterfSet,ValRange,简称 summary(ISR i ).其
中,VecNum 表示中断向量号,VarInterfSet 为中断 ISR i 对程序 P 的干扰变量集合,ValRange 为干扰变量值区间不