实时系统是指那些严格要求对外部的输入及时做出回应的系统.由于许多实时系统是高安全性系统,所以近几十年来,实时系统的模型验证已经成为研究热点之一.我们需要检验实时系统的两类性质:时段性质和瞬间性质,毫无疑问,检验实时系统的时段性质要比瞬间性质困难得多.目前使用的实时系统的模型检验工具大多都是检验实时系统的瞬间性质.在以前的相关工作中,由于问题的特性,我们发现检验实时系统的时段性质具有很高复杂度,很难在实际中应用.在该论文中,通过限制所要检验的问题来降低复杂度,目标是为了使检验实时系统某些时段性质的复杂度和检验瞬间性质相同.其中主要的研究工作如下:●考滤了在模型检验一般框架下时段性质的检验问题,在此基础上分析了在何时该问题可以转化成瞬间性质的检验问题,并进一步分析了转化后所得到问题的复杂度.●抽象出一类重要的实时系统时段性质:有序时段性质.有序时段性质是一类时段演算的公式,它表示系统在某些特定的位置轨迹上运行时需要满足的性质,经常出现在系统开发的设计阶段.●针对可用时间正则表达式表示其行为的实时系统的有序时段性质,根据对时间正则表达式结构的归纳,基于线性规划技术提出一个用来检验的算法,并对该算法进行了优化,该算法的复杂度是线性的.●对于时间自动机的有序时段性质,利用时间自动机的区域图,基于线性规划技术对其进行了检验,在此方法中通过整数化的技术大大减少了搜索的状态空间.这个方法和时间自动机的可达性问题(瞬间性质)具有同样的复杂度.