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

2984 Journal of Software 软件学报 Vol.32, No.10, October 2021

(a) (b)
Fig.8 Translation from a non-pure linear arithmetic logic to a DNF
图 8 非标准线性算术逻辑展开为析取范式

2.3 基于干扰变量的中断驱动程序顺序化

中断驱动是嵌入式软件设计常用的模式,由主程序和多个中断服务程序共同构成.在航天嵌入式软件中,通
常利用中断服务程序完成遥测数据采集、信息通信、遥控指令处理等功能.在中断驱动型程序中:中断机制具
有不确定性,即中断服务程序能够发生在主程序执行过程中的任一时刻,当中断发生后,会打断主程序正在执行
的操作转而执行中断服务程序;同时,中断机制还具有并发性,即主程序与中断服务程序之间交替执行.
针对第 1.2 节中断使用分析中提到的一类中断驱动程序,本文提出一种基于干扰变量的顺序化方法,该方
法的关键是采用抽象解释、摘要机制对中断函数特征表示,并基于干扰变量分析保证顺序化后的程序包含尽可
能少的中断函数.
2.3.1 中断驱动程序模型
中断驱动机制引起整数溢出错误主要是由于在中断服务程序中,对变量的操作影响了主程序中该变量的
取值.本文将中断驱动程序抽象为 4 类中断驱动程序模型,分别为 R-R 模型、W-R 模型、R-W 模型、W-W 模型
(如图 9 所示),并基于中断驱动程序模型分析中断服务程序对变量取值的影响.其中,x 表示程序 P 和中断向量号
为 i 的中断 ISR i 之间的共享数据单元,初值为 v 0 ;s i =v k ,l j 表示变量 x 在当前程序下的状态,即变量 x 在位置 l j 的
取值为 v k ;READ:x 表示当前程序位置下对变量 x 执行读操作;WRITE:x:=v i 表示当前程序位置下对变量 x 执行写
操作,将 v i 写入 x.
 R-R 模型:表示在 P 中对变量 x 执行读操作,在 ISR i 中对变量 x 执行读操作.此时,P 和 ISR i 执行路径中
每个状态上变量 x 的取值均为 v 0 ,说明在 R-R 模型中 ISR i 的执行并不影响 P 中变量 x 的取值;
 W-R 模型:表示在 P 中对变量 x 执行写操作,在 ISR i 中对变量 x 执行读操作.此时,P 执行路径上在 WRITE
前变量 x 的取值为 v 0 ,在 WRITE 后变量 x 的取值为 v 1 .ISR i 中并不改变变量 x 的取值,说明在 W-R 模型
中 ISR i 的执行并不影响 P 中变量 x 的取值;
 R-W 模型:表示在 P 中对变量 x 执行读操作,在 ISR i 中对变量 x 执行写操作.此时,由于在 ISR i 中对变
量 x 执行 WRITE 操作,使得 P 执行路径中状态 s 1 s 4 、s 5 s 8 上变量 x 的取值发生改变.说明在 R-W 模
型中,ISR i 的执行影响 P 中变量 x 的取值.进一步来说,对于 R-W 模型中的共享数据单元 x,P 中每次
READ 操作都要考虑 ISR i 中 WRITE 操作的影响;
 W-W 模型:表示在 P 中对变量 x 执行写操作,在 ISR i 中对变量 x 执行写操作.此时,虽然在 ISR i 中对变
量 x 执行 WRITE 操作,使得 P 执行路径中状态 s 1 s 4 上变量 x 的取值发生改变,但是 P 中通过 WRITE