检验实时系统的有序时段性质

摘要：

模型检验是一种被广泛应用于对设计或系统正确性进行自动验证的技术.实时系统的性质包括瞬间性质和时段性质,显然后者的检验要比前者复杂得多.介绍了一类新的时段性质--有序时段性质,并检验了时间正则表达式的有序时段性质,最后分析了算法的复杂度,和相关工作进行了比较,并探讨了今后的工作方向.

关键词：模型检验、实时系统、有序时段性质、时间正则表达式

所属期刊栏目：39

分类号：TP301.1;TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金6027036;江苏省自然科学基金BK200209

在线出版日期：2008-05-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：476-489