中断驱动系统(Interrupt-driven System)被广泛应用于安全关键系统中,因而中断驱动系统的正确性保障尤为重要。此类系统通常使用操作系统任务调度加中断处理程序的软件体系结构。系统中的中断事件的发生时间及顺序具有极大的不确定性,不同的中断发生时间和顺序将导致不同的系统行为,而系统中的许多设计错误只有在特定的处理顺序下才会显现出来。因此在中断驱动系统的设计和开发过程中,测试工作开销极大且效率低下,需投入很大的精力用于错误的重现与定位,大量的测试工作只能定位少数错误,系统的正确性得不到保障。模型检验(Model Checking)技术的出现使得全面分析和验证中断驱动系统的系统行为成为可能。其基本思想是对待验证系统进行形式化建模,用模型的运行来模拟系统运行,然后利用计算机的快速计算能力,穷举被验证系统的状态空间中的每一个状态来验证该系统是否满足特定的形式规约。在过去的工作中,我们提出了中断驱动系统的有界模型检验方法,其核心是以时间自动机+伪代码建立中断驱动系统的形式化模型,然后用深度优先的方式进行状态空间遍历。实践证明,该方法能够切实有效地检测出中断驱动系统中的错误。但随着中断驱动系统中中断数量的增长,模型状态空间呈指数级增长,使得检验过程的时间花费极高。偏序约减(Partial Order Reduction)技术通过消除并发系统中由于迁移交错执行而产生的冗余的遍历路径来达到约减状态空间的目的,是一种常用的提高模型检验算法效率的方法。本文通过对中断驱动系统所具有的特性的分析,在原有有界模型检验算法的基础上,提出了基于偏序约减技术的优化算法。实验证明,该优化算法能够大幅提高中断驱动系统模型检验的效率。本文的主要工作如下:1.实现了中断驱动系统的有界模型检方法。本文采用时间自动机+伪代码的建模方式对中断驱动系统建模,并将系统中的时间约束和系统规约编码为线性不等式组,调用SMT(Satisfiability Modulo Theories)求解器Z3求解。实践证明该方法能够应用于实际中断驱动系统的模型检验,并能有效检测出系统中的错误。2.提出了一套完整的、切实可行的基于偏序约减技术的优化方案。我们首先对模型的运行方式进行了重新定义,将中断的触发、响应与执行整合为一个事件,确定偏序关系的粒度。在进行验证前,首先通过静态分析,得到中断处理程序间的依赖关系。在状态遍历过程中,将多个同时满足触发条件的中断根据相互之间的依赖关系生成偏序路径,然后按照偏序路径执行到达新的状态。由于偏序路径排除了其它等价的路径,所以此优化算法能够消除冗余的遍历路径,达到约减状态空间的目的。3.将优化方案应用到模型检验工具中并进行了实例研究。实验结果表明,本文提出的优化算法能够有效约减状态空间、减少验证时间。而且,随着系统中中断数量的增加,优化算法的效果更加明显。