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

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

(2) 与其他两款工具相比,本文方法误报数略高.对所有被测程序检测误报总数进行分析,Polyspace 和
SpecChecker 的误报总数分别为 7 个和 12 个;而本文方法的误报总数为 13 个,误报数略高,误报分析
将在后文中给出详细描述;
(3) 与 SpecChecker 相比,本文方法检测时间较长.对所有被测程序检测总时间进行分析,使用 SpecChecker
工具的检测时间为 13.69s,而本文方法的检测时间为 45.69s.这是由于,经顺序化操作后程序规模变大,
导致有界模型检测时间增加,并且检测时间增长量与干扰变量的个数以及插入中断的次数密切相关,
因此,如何进一步缩短中断驱动程序整数溢出检测时间、提高方法可用性,是未来的研究方向之一.
Table 5 Fault information of aerospace embedded software
表 5 航天嵌入式软件错误信息
被测程序 整数溢出总数 整数溢出类型 出错原因
中断中将共享变量清零,退出中断后在主程序中
ALTU 1 无符号整数下溢
对该变量进行减 1 操作,导致整数溢出
中断中对共享变量 count 进行累加操作,
主程序中循环执行如下语句:
mwcur=count;
SIFU 1 无符号整数下溢 mwsend=mwcurmwlast;
mwlast=mwcur;
若共享变量 count 累加后溢出(属于正常设计),
则主程序中会发生小数减大数的整数溢出错误

Table 6 Analysis results of instance verification
表 6 实例验证实验结果
软件 logger blink brake ic2_pca_isa i8xx_tco wdt_pci ALTU SIFU 合计
规模/LOC 161 164 819 321 757 1 339 904 1 985 6 450
中断数 2 3 2 4 3 8 4 3 29
整数溢出错误 3 2 3 2 2 4 1 1 18
命中数 1 1 1 0 1 2 0 0 6
Polyspace 误报数 0 0 0 0 0 0 1 6 7
检出时间(s) 4.00 6.00 10.00 6.00 9.00 13.00 11.00 18.00 77.00
命中数 2 1 1 0 2 3 0 0 9
SpecChecker 误报数 0 0 0 0 0 0 4 8 12
检出时间(s) 0.34 0.33 0.62 0.45 0.78 4.15 0.54 6.48 13.69
命中数 3 2 2 1 2 3 1 1 15
本文方法 误报数 0 0 0 0 0 0 2 11 13
检出时间(s) 0.97 0.73 2.33 1.17 0.80 5.82 0.37 33.50 45.69
本文对所有误报进行了分析,发现本文方法误报的主要原因是:某些干扰变量取值范围仅在软件需求中进
行约束,而在程序中缺少相关条件判定,经中断函数特征抽象后,该干扰变量取值区间大于需求中规定的取值范
围,经有界模型检测后引起误报.图 11 给出了此类误报的典型样例,样例中,数组 uartSend 类型为无符号字符型.
本文方法报告 S 1 处发生无符号整数上溢,即:在循环累加过程中,累加值超出了无符号字符型整数取值范围.在
实际程序运行中,从地址 XBYTE[0x002D],XBYTE[0x002E]取值内容受需求规范约束,使得 S 2 和 S 3 处的变量
uartSend[2]和 uartSend[3]被赋值后,参与 S 1 处的累加操作时不会产生整数溢出,因此该整数溢出为误报.
本文方法通过对中断 ex0_ISR 中的干扰变量 uartSend[2]和 uartSend[3]值区间不变式进行迭代分析,计算出
上述变量取值范围为[0,0xFF],经顺序化后进行有界模型检测,报告 S 1 处发生整数溢出.虽然仅从代码分析角度
来看确实存在发生整数溢出的风险,但是从软件功能分析角度来看,该处不可能发生整数溢出.因此,下一步我
们将探索更精确的中断特征抽象技术来消除该类误报.