实时系统的模型检验中针对共享变量的优化技术

实时系统可以使用由多个并发的时间自动机组成的时间自动机网络来建模。网络中的时间自动机通过共享变量和/或信道交互。带有不同共享变量取值的自动机网络的状态是截然不同的。因此，共享变量也是引起状态空间爆炸问题的原因之一。本文提出了在不同共享变量取值之间的兼容性关系的概念。使用这种兼容性关系，时间自动机网络的可达性分析算法就可以减少需要遍历的状态的个数。本文给出了检测符号化状态中共享变量的取值所能兼容的其它取值的算法以及进一步进行这种兼容性关系检测的增强算法。最后还给出了使用了这两种算法进行优化之后的可迭性分析算法。实验结果显示经优化的可达性分析算法的空间效率得到了显著的提高。

Optimization Technique for Shared Variables in Real-time System Model-Checking

Real-time systems are often modeled as timed automaton networks, which are parallel compositions of timed automata. Those timed automata interact with each other through shared variables and/or communication chan- nels. In the literate, symbolic states with different shared variable valuations in automaton networks are treated as distinct ones. Therefore, shared variables are also one of the causes of state-space explosion. We present the notion of the compatibility relationship between different shared variable valuations in this paper. Using this compatibility relationship can reduce the amount of states that need exploring in the reachability analysis algorithm of timed au- tomaton networks. In this paper, we describe two algorithms: one that detects compact shared variable valuations and the other more powerful one that detects this compatibility relationship further. These two algorithms result in an enhanced reachability analysis algorithm. The experiment results show that our technioque improves the space-effi- ciency of reachability analysis significantly.