论文部分内容阅读
时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。
Time automaton is a computational model that effectively describes real-time system behavior. Real-time system analysis with timed automata designed to ensure that the development of real-time systems with high reliability. The verification of time automata in this process is a crucial step. The main purpose of verification is to ensure that time automata correctly describe real-time systems. Among them, the satisfiability of time constraint of migration is one of the properties that needs to be verified. A common approach is to construct time-domain automata, but the number of states involved in this approach is huge. Aiming at the characteristics of a class of timed automata, this paper gives a method to determine the satisfiability of time constraints based on the time relation matrix. The results show that this method can effectively reduce the number of states.