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

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

Table 2 Fault code in tcas program
表 2 tcas 程序中的故障代码
序号 故障代码 溢出类型 代码行号
unsigned int Positive_RA_Alt_Thresh[4]; 27
1 无符号整数上溢
return Positive_RA_Alt_Thresh[Alt_Layer_Value]*5804010; 58
unsigned int alt_sep=0; 116
2 无符号整数下溢
alt_sep=alt_sep1; 122
Up_Separation=nondet_int(); 165
3 有符号整数上溢
return (Climb_Inhibit?Up_Separation+NOZCROSS:Up_Separation) 63
Up_Separation = nondet_int(); 165
4 有符号整数下溢
return (Climb_Inhibit?Up_Separation+NOZCROSS:Up_SeparationNOZCROSS) 63
在样例验证过程中,设置界限 k 为 3,对以上被测程序进行整数溢出检测,并对程序模型约简前后的结果进
行对比,实验结果见表 3.
Table 3 Analysis results of sample verification
表 3 样例验证实验结果
分析结果
被测程序 布尔变量数 子句数 检测时间(s) 问题命中数
约简前 约简后 约简前 约简后 约简前 约简后 约简前 约简后
tcas 3 083 1 803 6 967 5 271 0.06 0.03 4 4
schedule 176 915 120 605 310 125 223 980 2.32 1.86 5 5
schedule2 2 047 412 1 294 648 3 883 800 2 548 033 24.26 14.16 4 4
printtokens 445 260 192 138 3 244 408 2 053 365 8.89 5.64 6 6
从表 3 的实验结果可以看出:在保证问题检出效果的同时,约简后的布尔变量数、子句数以及检测时间相
对于约简前大幅度降低.以 tcas 程序为例,其整数溢出检测时间下降 50%.这表明,本文提出的约简技术是行之有
效的.
3.2 实例验证
实例验证阶段,由于文献[14]介绍的基准测试程序内置故障不包含整数溢出,因此本文通过变异注入的方
式构造整数溢出错误,而选取的真实航天领域嵌入式软件均属于安全关键的中断驱动型程序.被测软件描述信
息见表 4.
Table 4 Description of programs used in our experimental evaluation
表 4 被测软件描述信息
被测程序 描述信息 来源
logger 温度记录固件建模程序,包括两个中断处理函数,分别用于测量和通信
blink LED 灯控制程序,通过检查计时器值控制 LED 灯闪烁
由 Matlab/Simulink 仿真模型生成的刹车系统程序,中断
brake
处理函数主要用于根据每个轮子的速度计算制动扭矩 基准测试程序
ic2_pca_isa Linux 内核驱动程序,用于支持 ISA 板功能
i8xx_tco Linux 内核驱动程序,用于支持 i8xx 芯片组的 TCO 定时器功能
wdt_pci Linux 内核驱动程序,用于支持看门狗功能
ALTU 用于动量轮脉冲信号采集以及动量轮、磁力矩器、自锁阀等的电源切换 航天嵌入式软件
SIFU 用于完成星上天线伺服控制功能
本文选取的两个真实航天嵌入式软件分别存在一个受中断使用引发的整数溢出错误,错误信息见表 5.
在实例验证过程中设置界限 k 为 3,使用本文方法对以上被测程序进行整数溢出检测,并分别与两款商业工
具 polyspace 2016b 以及 SpecChecker 2.3.2 的结果进行对比,实验结果见表 6.从表 6 的实验结果可以看出:
(1) 本文方法能够有效地检测整数溢出错误.对比其他两款工具,本文方法命中总数为 15 个,并且正确检
出了真实航天嵌入式软件所包含的全部整数溢出错误,这表明,本文方法针对中断引起的整数溢出检
测是非常有效的;