梁 昊 艾云峰 沈怀荣 赵永超

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



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

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

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

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

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

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