满足各种时间约束是实时嵌入式系统设计的一个重要目标。通常,时间约束要求实时系统在满足功能性需求的同时,还必须保证系统行为的时效性,即系统必须在确定的时间内执行其功能。中断机制是嵌入式系统进行实时响应的重要机制,它允许外部事件打断系统的执行,立即转向执行对事件进行处理的程序。实时系统的设计需要综合运用任务调度和中断机制,以保证具有时间关键特性的功能及时得以执行。针对给定的时间约束,如何基于可抢占任务调度机制和中断机制设计系统,是嵌入式系统设计需要解决的核心问题之一。嵌入式系统的实际运行轨迹是任务调度机制、中断机制、中断源特性以及代码执行时间等多个因素综合作用的结果,是一个无穷的集合。目前还不存在一种有效地中断驱动系统设计方法来保证系统的时间约束总能够得到满足。因此,目前保证系统实时性的方法主要依靠在设计完成后,对设计好的系统能否满足时间约束进行验证。针对周期性中断源驱动的实时系统,本文研究了基于线性混成自动机对其执行行为和时间约束进行建模的方法。通过将中断驱动系统的时间约束的验证问题转换为线性混成自动机的可达性问题,给出了基于面向路径可达性验证技术和基于有界可达性验证技术的时间约束验证方法。线性混成自动机的可达性问题是不可判定的,基于带一个停表的时间自动机,我们给出中断驱动系统的的一个可判定子类——两级中断系统,并给出其上时间约束的验证方法。具体的,本文的主要工作如下：1.提出了一个基于线性混成自动机为周期性中断源驱动的实时系统进行建模的方法。分析了此类系统的建模需求,以及中断时间自动机建模方法的局限性。实时系统的模型中,通过定义多个停表实数变量来累计各个任务执行被打断时的执行时间以及执行恢复后的执行时间,通过定义停表变量之间的优先级来模拟中断机制；中断源的模型中,通过定义全局时钟变量来描述多个中断源周期性发生的情况。将系统模型和中断源模型进行组合,构造出系统最终的模型。2.以线性混成自动机模型为基础,研究了基于面向路径可达性验证技术和有界可达性验证技术对时间约束进行验证的方法。将中断驱动系统的时间约束验证问题转换为线性混成自动机上的可达性问题,对系统的时间约束进行验证。基于面向路径可达性验证技术的时间约束验证方法的主要思想是通过提前构建不满足系统规约的路径集,将系统的时间约束问题转换为线性混成自动机上的这些路径的可达性问题；而基于有界可达性的时间约束验证方法,通过将系统的行为限制在有限的k步之内,对该步长之内的系统构建完整的状态空间,来检验在k步之内系统是否满足给定的时间约束。3.基于带一个停表的时间自动机模型构建了周期性中断源驱动的实时系统的一个可判定子类——只包含两级中断的实时系统,并研究了其上时间约束的验证方法。通过构建该系统模型的等价状态类图,将只包含两级中断的实时系统的时间约束问题转换为等价状态类图上的可达性问题,借助于图的搜索算法对其时间约束的满足情况进行有效地判定。该方法的复杂度为O[(|Q|+|E|)·2δ(N)],其中|Q|是为系统模型中位置节点的个数,|E|为系统模型中迁移关系的个数,δ(N)是对模型中约束条件中实数的编码长度。