中断驱动系统被广泛应用于安全关键的嵌入式系统中,如航空航天、工业过程控制等。这些系统对软硬件的可靠性要求极为苛刻,一旦出现系统错误或失效会造成重大经济损失、大规模环境破坏、甚至人员伤亡等严重后果,因此保证中断驱动系统的可靠性是非常重要的。在中断驱动系统中,中断发生的不确定性和中断嵌套使得系统行为十分复杂,而系统中潜在的错误行为可能只有在特定的中断触发时序下才能显现出来。现有的基于测试的方法无法对中断驱动系统提供全面的检查,难以保证中断驱动系统的可靠性。基于模型检验的验证方法虽然可以完全验证模型所表示的系统行为,但现有的建模方法的使用都较为困难,影响其实用性。为此,本文提出了一种基于场景的中断驱动系统建模与验证方法,它包括中断驱动系统的建模和模型验证两个方面:在中断驱动系统建模方面,我们提出了一种基于中断序列图的中断驱动系统建模方法。中断序列图是对UML序列图的扩展,其中包括:1)新增中断组合片段,用于对中断任务建模;2)在交互事件上引入变量赋值操作,用于控制中断的触发条件;3)扩展时间约束表达,增强序列图对系统的实时性需求描述。中断序列图能够简单直观地描述中断驱动系统中的系统任务和中断任务,并且能够刻画出中断发生的不确定性和抢占性等特征。在模型验证方面,首先我们使用中断序列图构建中断驱动系统模型,然后将中断序列图转换成与之语义等价的混成自动机网络,最后使用混成自动机验证工具SpaceEx,针对中断驱动系统中的任务超时和数据一致性问题进行验证。基于上述方法,我们实现了中断驱动系统建模与验证工具ISDChecker,它提供了可视化的用户接口,能够帮助系统设计人员快速地构建基于中断序列图描述的中断驱动系统模型。使用该工具,我们进行了案例研究,验证了本文方法的有效性。