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

【Abstract】 Model checking is an automatic technique for verifying finite-state concurrent systems. It is a well-established and easy-to-use approach to checking whether a system satisfies some properties. Model checking tools have been widely accepted in industry for aiding system design. Any system where a timely response by the computer to external stimuli is vital is a real-time system. Due to the nature of real-time systems, errors in them maybe extremely dangerous, and even fatal. There are two kinds of properties of real-time systems: instant properties and duration properties. Without doubt, checking real-time systems for a duration property is much more difficult than for an instant property. In this paper, we propose a new kind of duration properties: temporal duration properties. Temporal duration properties form another class of duration calculus formulae. They require the system satisfy some linear inequalities on integrated durations of system locations when the system runs following some location traces, and are often met in the development of real-time systems using duration calculus. An algorithm is developed to check whether a temporal duration property is satisfied by a real-time system of which the behaviors can be represented by a timed regular expression using linear programming, and some improvements on the algorithm are given. We also analyze the complexity with comparison of some related work, and discuss the future work in the end.更多还原