航天软件中多重中断程序的动态检测方法研究

梁 昊 艾云峰 沈怀荣 赵永超

1.装备学院研究生管理大队，北京 101416 2.中国科学院大学工程管理与信息技术学院, 北京100049 3.装备学院航天装备系，北京 101416 4.国防大学作战与指挥训练教研部, 北京 100091



航天软件中多重中断程序的动态检测方法研究

梁 昊1艾云峰2沈怀荣3赵永超4

1.装备学院研究生管理大队，北京 101416 2.中国科学院大学工程管理与信息技术学院, 北京100049 3.装备学院航天装备系，北京 101416 4.国防大学作战与指挥训练教研部, 北京 100091

随着控制系统软硬件平台的设计复杂度不断增加，特别是飞行控制系统中集成的传感器不断增多，中断数量也随之不断增加。本文根据飞控系统的具体特点，使用标记迁移系统对多重中断并发程序进行建模，提出了原子性违背和数据竞争的形式化描述，运用动态偏序化简算法对程序的状态空间进行化简，并设计实现了多重中断控制系统程序的动态检测工具，实验结果表明该检测算法可以在满足对多重中断并发程序错误检测的基础上，大大的缩短检测时间。

多重中断；数据竞争；原子性违背；偏序化简

当前多重中断程序在航空航天控制软件，特别是在飞行控制软件中得到了广泛应用。由于中断嵌套的原因，多重中断程序的执行路径存在大量交叠，使得程序的运行过程具有强烈的复杂性、不确定性和难以预期性，这给航空航天控制软件设计与测试工作带来了大量的困难。研究者针对多重中断程序的错误检测已经展开了一系列的研究，提出了静态分析和动态验证2种主要的测试方法。

静态分析的基本原理是不编译运行程序，将程序抽象成模型，对模型中共享对象的读写操作进行检查，如GOBLINT[1]和国防科技大学设计的MIDAC[2]检测工具。静态测试主要缺点在于无法避免“状态空间爆炸”和误报率较高的问题。

动态验证方法的基本原理是利用给定测试数据，驱动被测试程序执行，并在执行的过程中对程序进行验证。该方法可有效的避免可执行程序代码(包括编译、运行连接库等)与程序模型之间存在的不一致问题。与静态分析相比较，动态验证不会产生误报，同时可避免复杂的建模、语义差异和约束求解。VeriSoft[3]是一个采用动态验证方法的典型测试工具，它面向可执行程序，能够验证由C，C++，Tcl等语言编写的可执行代码。计算机技术与应用研究所提出的多重中断程序测试框架[4]也是一种动态测试工具，它的主要设计思想是对中断进行两两对比测试，通过不断提高2个中断的触发频率来加速并发错误的出现。但是该方法只能针对2个外部中断进行独立测试，且需要人为干预，无法保证测试的覆盖率。

文献[5-6]所采用的类线程测试方法为多重中断的测试提出了新的思路，其主要原理是将中断程序改写为“语义”等价的多线程程序，然后使用Locksmith races以及cXprop race对多线程程序进行测试。但该方法在对多重中断程序进行改写后，需要操作系统的内核支持，而控制软件特别是飞行控制软件多使用无操作系统的多重中断设计方式，因此该方法在工程应用方面存在无法弥补的弊端。

本文在参考了国内外已有技术的基础上，将用于多线程并发程序验证的基于Happens-Before关系的动态偏序化简思想在功能上进行了延伸和拓展，使其可以处理不基于操作系统的多重中断程序。首先描述了多重中断程序的系统建模，并给出了原子性违背和数据竞争两种并发错误的形式化描述；然后介绍了动态偏序化简算法，之后对该算法进行改进，使之可以对多重中断程序进行测试，并介绍了该算法中的并发错误检测模块；最后通过实验对比证明了所提出的动态验证方法在实际程序测试方面的准确性和有效性。

1 多重中断程序建模与并发错误定义

1.1 多重中断程序建模

本文使用了标记迁移系统对多重中断并发程序进行建模，标记迁移系统(Labeled Transition Systems, LTS)[7]的具体描述如下：

定义1 LTS(标记迁移系统)是一个四元组M=(S,init,T,R),其中：S表示并发程序的状态集合；init表示初始状态(也可表示为s0)，并且有init∈S；T表示迁移集合；R表示迁移关系集合。

在控制软件中，往往包含1个主函数main和若干中断服务函数interrupts。本文将由main函数和其调用的普通函数记作一个整体，将中断服务函数的标记集合为IR，则多重中断程序的整体标识集合为：Fid={main}∪IR，fid∈Fid,该标识对应于每一个具体的函数(中断服务函数或者main函数)。

不同中断服务函数对于全局共享对象的读写操作，称之为可见操作，对于不同中断服务函数中本地对象的读写操作，称之为不可见操作。由于不可见操作对共享变量没有影响，因此下文中只对可见操作进行讨论。

1.2 多重中断程序中并发错误定义

在描述多重中断程序并发错误之前必须首先介绍2个相关概念。

定义4R∈T×T是独立关系，当且仅当对于每一个∈R，如果它们是相互独立的，则必须满足下面2个关系：

独立关系的定义反映了迁移t1,t2作用于同一个全局状态中2个不同的局部状态；或者t1,t2是作用于同一个局部变量上的2个读操作，此时交换它们的执行次序对程序的运行无影响。

1.2.1 原子性与原子性违背

原子性的定义[8]：一个事务中的所有操作，要么全部完成，要么全部不完成，不会结束或中断在某一个环节，事物在执行过程中发生错误会被回滚到初始状态。

多重中断中C语言程序的原子性违背的形式化描述为：给定1个原子块A，它的迁移序列为：TA={t1,t2,…,tn}，∃i∈[1,n],ti∈TA，即ti处在原子块A中，原子块中所有写操作的集合OPW(A)={op|op∈OP(A),and,op(A)=write}，原子块中所有读操作的集合OPR(A)={op|op∈OP(A),and,op(A)=read}，其中op的含义为操作；OP(A)为原子块A中所有可见操作的集合。如果∃t∉TA，并且t与ti是非相互独立且可同时执行的迁移，若(OPR(A)∩opw(t))∪(opr(t)∩OPW(A))∪(OPW(A)∩opw(t))≠φ，则会引发原子性违背错误。其中opw(t)，opr(t)分别表示op(t)=write，op(t)=read。

1.2.2 数据竞争

数据竞争的定义[9-10]：2个线程在没有同步操作保护的前提下同时访问一块共享内存，且至少其中有一个访问为写操作。

多重中断中C语言程序数据竞争的形式化描述为：对于程序中的任意一个状态s，在其上的所有写操作的集合为：OPW(s)={op|op∈OP(s),and,op(s)=write}，所有读操作的集合为：OPR(s)={op|op∈OP(s),and,op(s)=read}，如果存在2个迁移t和t′在状态s上都是可执行且非相互独立的，若t和t′分别属于2个优先级不同的中断函数，t和t′有一个操作在集合OPW(s)中，则状态s存在数据竞争错误。

数据竞争与原子性不同，原子性定义的描述必然是针对多个并发程序状态而言的，即这个代码段内包含了一系列的状态和迁移；而数据竞争主要针对一个状态和这个状态的可执行迁移而言。

2 面向多重中断程序的动态验证算法设计

2.1 动态偏序化简

上文已经提到，控制系统并发程序在动态执行的过程中状态空间会变得极其巨大，甚至出现状态空间爆炸的问题。为此本文将基于Happens-Before关系的多线程程序动态偏序化简(Dynamic Partial-Order Reduction，以下简称DPOR)[11-12]方法引入到多重中断程序的状态空间化简中。

动态偏序化简的主要思想就是计算各个状态的Persistent 集合。但传统的DPOR算法在处理多重中断程序中有2个缺陷：1)无法对包含无限循环的程序进行化简[11]，而控制系统的并发程序往往会普遍使用有无限循环的设计方式；2)DPOR算法无法对包含优先级的中断服务函数作出处理。

2.2 面向多重中断的动态偏序化简算法

针对2.1节中提出的问题，本文在传统的基于persistent集合的DPOR算法基础上，引入了sleep集合的概念。一个状态s的sleep集合表示在状态s上可执行但又没有必要执行的迁移的集合，记为s.sleep。引入sleep集合可以进一步排除DPOR算法对相互独立关系迁移的选取，同时将被检索过的迁移加入sleep集合，可以避免DPOR算法反复搜索已经执行过的迁移，这点对含有循环的程序格外重要，它可以减少s.enabled集合中的迁移，从而避免由无限循环所带来的程序状态空间的无限制增长，如图 1中的第32行所示。

图1 DPOR算法描述

图1的算法设计中，采用基于深度优先的搜索方法来对程序的状态空间进行搜索。算法中使用集合FID来代表程序的函数空间，fid即为函数的唯一标识，fid(s)返回动态执行过程中状态s所处的当前函数标识，fid(t)返回迁移t所在的函数标识。PRI的作用是记录函数的优先级，中断服务函数的优先级为其自身的优先级，main函数的优先级最低。通过在图 1中第8，13，15行中，加入对函数优先级的比较，实现了高优先级的中断服务函数可以打断低优先级的中断服务函数和普通函数的执行，这样还可以进一步缩减动态执行中的目标程序状态空间。

在DPOR算法中，控制执行器记录了包含全局对象的搜索堆栈S，s.backtrack为回溯集合表示需要搜索的状态s的线程集合。s.done表示被检测过的状态s的线程集合，函数UPDATEBACKTRACESETS(S,t)的作用是动态计算persistent集合，给定一个状态s，状态s的persistent集合不会在程序到达状态s后立即被计算出来，而是在状态s下使用深度优先搜索的算法对persistent集合进行计算。算法的具体描述如图2所示。

图2 UPDATEBACKTRACESETS算法描述

函数UPDATEBACKTRACESETS算法与经典DPOR的回溯算法相同，只是在图 2的第4行中，加入对于函数fid(td)的中断允许标志位的判断，如果该中断没有被使能，则计算在状态sd的回溯集合。关于DPOR的算法的详细理论与数学证明请参考文献[11]。

2.3 多重中断程序并发错误检测算法

在图 1所描述的算法中，函数DETECTERROR的作用是在状态s处检测是否存在原子性违背和数据竞争错误，其算法实现如图 3所示。

图3 多重中断程序并发错误检测算法

图 3中第2～14行，按照文中对原子性违背形式化描述，设计了并发程序原子性违背错误检测方法，主要是检测多重中断程序中多变量读写时是否存在原子性违背错误；第15，16行主要是检测程序执行过程中，高优先级中断打断低优先级中断时，程序是否存在数据竞争的情况。

3 实验平台和实验结果

3.1 实验平台

多重中断程序动态测试工具构架主要包含4个部分：程序分析器、中断服务函数分析器、控制执行器和中断发生器。

图4 多重中断测试工具设计框架图

中断服务函数分析器的主要作用是识别程序的内部和外部中断，建立中断触发机制。控制执行器的主要工作是接收由插装、编译后的被测试程序得到共享变量、函数注册信息，并根据以上信息控制中断发生器的中断引号产生时间，在目标程序执行的过程中，使用DPOR算法对状态空间进行化简，同时根据不同路径的交叠执行情况，判断并发交叠中是否包含数据竞争、原子性违背错误。中断发生器的作用是在控制执行器给定的信号驱使下，产生相应的中断，对于内部中断不进行触发，而是等待条件允许后，内部中断自身完成触发执行。目标机的作用是接收中断信号，动态执行被测试程序。

3.2 实验结果

表1 测试软硬件平台

被测试程序方面，选用了基于DSP的飞行控制程序，基于AVR单片机的四旋翼飞行器控制程序。为了通过实验验证控制系统并发程序错误检测算法的执行效率，对目标程序的中断数量进行了修改。具体的实验结果如表2所示。

表2 实验结果

在以上的表格中，用“/”表示程序无法在24 h(86400s)内测试完成。从表 3可以看出，被测程序包含的中断数、搜索迁移数和检测时间等3个比较指标，在使用了偏序化简算法以后，执行时间大大缩短，提高了检测效率。

表3中由于多重中断测试框架只能对中断服务函数进行两两比对测试，只能通过手动来完成全部的测试，所以无法统计测试时间。在类线程的测试方法中，由于其需要操作系统内核的支持，所以DSP平台无法完成测试，在AVR平台中，本文使用了TinyOS操作系统来完成类线程测试。通过实验结果的对比，可以看出相对类线程测试本文设计的检测算法拥有更高的检测效率，而且在AVR3的试验中不但找到数据竞争的存在，而且还发现了一个原子性违背错误。

表3 实验结果

4 结束语

根据控制系统中多重中断并发程序的相关特点，将基于线程的并发C语言程序状态空间DPOR化简算法应用于多重中断程序的状态空间化简，极大地缩短了测试执行时间。根据原性子违背和数据竞争的经典定义，在标记迁移系统中给出了这两种并发错误的形式化描述，并完成对原子性违背和数据竞争检测的算法设计，最终实现了对于包含多重中断控制系统的并发错误检测。由于检测算法基于Happens-Before关系，因此在数据竞争的检测方面，可以报告出存在的数据竞争，但还无法区分是良性的数据竞争还是恶性的数据竞争。

[1] Hatcli J Robby, Dwyer M B. Verifying Atomicity Speci-fications for Concurrent Object-oriented Software Using Model-checking[C]//LNCS 2937: Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004), Venice, Italy, Jan 11-13, 2004. Berlin, Heidelberg: Springer-Verlag, 2004: 175-190.

[2] 吴学光，文艳军，王戟,等.多重中断数据竞争及原子性违背检测[J].计算机科学与探索,2011,12(3):1086-1093.(Wu Xueguang, Wen Yanjun, Wang Ji, et al. Data Race and Atomicity Checking for C Programs with Multiple Interruptions[J]. Journal of Frontiers of Computer Science and Technology,2011,12(3):1086-1093.)

[3] Juergen Dingel. Computer-Assisted Assume/Guarantee Reasoning with VeriSoft[C]. In Proceedings of the 25th International Conference on Software Engineering(ICSE'03). Washington, DC, USA: IEEE Computer Society press,2009:138-148.

[4] 傅修峰，陈丽容.多重中断程序测试框架[J].计算机工程与设计,2012,2(2):617-623.(Fu Xiufeng, Chen Lirong. Frameork for Testing Multiple Interrupts Program[J]. Computer Engineering and Design, 2012,2(2):617-623.)

[5] John Regehr, Nathan Cooprider. Interrupt Verifition via Thread Verification[J]. Electronic Notes in Theoretical Computer Science, 2007,174(9): 139-150.

[6] Wanja Hofer, Daniel Lohmann, Fabian Scheler, et al. Sloth: Threads as Interrupts[C]. Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS ’09) Washington, DC, USA: IEEE Computer Society Press, 2009:215-228.

[7] Chaki S, Clarke E M, Ouaknine J, et al. Automated, Compositional and Iterative Deadlock Detection[C]. Proc. of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-design. Washington, DC, USA: IEEE Press, 2004: 201-210.

[8] Abraham Silberschatz, Peter Baer Galvin, Greg Gagne. Operating System Concepts (8th Edition)[M]. 2009 John Wiley & Sons, Inc:733-734.

[9] Netzer R H B. Race Condition Detection for Debugging Shared-Memory Parallel Programs[D].Madison, WI, USA: University of Wisconsin, 1991.

[10] Netzer R H B. What are Race Conditions? Some Issues and Formalizations[J]. ACM Letters on Programming Languages and Systems,1992,1(1):74-88.

[11] Cormac Flanagan , Patrice Godefroid. Dynamic Partial-order Reduction for Model Checking Software[C]. In Proceedings of POPL’05,Long Beach, California, USA: ACM press, 2005:110-121.

[12] Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem [M]. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1996:27-78.

DynamicTestingMethodforProgramwithMultipleInterruptsinAerospaceSoftware

LIANG Hao1AI Yunfeng2SHEN Huairong3ZHAO Yongchao4
1. Company of Postgraduate Management, the Academy of Equipment, Beijing 101416, China 2. College of Engineering & Information Technology, University of Chinese Academy of Sciences, Beijing 100049, China 3. Department of Space Equipment, the Academy of Equipment, Beijing 101416, China 4. National Defense University, Department of Battle Command and Training, Beijing 100091, China

Inrecentyears,withincreasingdegreeofdesigncomplexityoncontrolsystem,especiallyforflyingcontrolsystemintegratedwithincreasingnumberofsensors,thereisagrowingnumberofinterruptsincontrolsystem.TheLTSisusedasthesystemmodelinmultipleinterruptionsprogram,theformaldescriptionforatomicityviolationanddataraceispresented,theDPORalgorithmisusedtoreducethespaceofprogramstateandthedynamictestingtoolisdesignedforcontrolsystemunderthemultipleinterruptions.Atlast,theexperimentalresultsshowthatthistestingmethodcannotonlytestdugforthemultipleinterruptprogram,butalsocanlargelyreducethetestingtime.

Multipleinterrupt;Datarace;Atomicityviolation; DPOR

2014-03-11

梁昊(1981-)，男，北京人，博士研究生，主要研究方向为兵器发射理论与技术；艾云峰(1979-)，男，济南人，博士，副教授，硕士生导师，主要研究方向为嵌入式系统实践、实时嵌入式操作系统、智能交通、嵌入式系统建模与测试；沈怀荣(1954-)，男，安徽舒城人，博士，教授，博士生导师，主要研究方向为兵器发射理论与技术；赵永超(1982-)，男，石家庄人，博士后，主要研究方向为装备论证作战数据与作战模拟。

TP311.5

： A

1006-3242(2014)05-0059-06