自动验证并发实时系统的线性时段性质

AUTOMATICALLY CHECKING REAL-TIME SYSTEMS FOR LINEAR DURATION PROPERTY

介绍了一个就线性时段特性验证实时系统正确性的工具的设计思想以及相关算法 .使用时间自动机作为实时系统的描述模型 .同时 ,为了便于描述并发实时系统 ,使用带共享变量和通道的时间自动机网作为模型描述并发实时系统 .在检验时间自动机网时 ,用户可以使用工具提供的合成程序将其合并为一个时间自动机然后进行检验 .由于时间自动机的状态空间是无穷的 ,通过引入整数状态和状态等价关系的概念 ,将整个状态空间划分为有限的状态等价类空间 .模型检验过程只需要通过对等价类空间的搜索就可以完成 .但往往等价类空间的规模很大 ,超出了现在计算机的处理能力 ,原始搜索算法仅仅在理论上是可行的 .为了增强工具的使用性 ,工具中使用的算法运用了一些优化技术来避免对等价类空间的穷尽搜索 ,使得工具在使用时具有比较好的时间和空间效率 .

In this paper, some design ideas, as well as some related algorithms, of a tool on checking a real-time system for a linear duration property are presented. Timed automata are used as the model language for real-time systems. Networks of timed automata with shared variables and channels are introduced as model language for concurrent real-time systems. Users can compose a network into a timed automaton through the composition program available in this tool when checking the network. Considering the infinite state space of a timed automaton, the concepts of 'integral state' and 'state equivalence' are introduced in this paper to divide the infinite state space into finite number of equivalence classes. Then the model can be checked through exploring the space of equivalent classes. However, the number of equivalence classes is generally too large for a computer to manipulate, so the primitive search algorithm is only theoretically feasible. In order to enhance the tool's ability, the algorithms in this tool adopt some techniques to avoid exhaustive exploring the space in order to get better time- and space-efficiency.