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

摘要：

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

关键词：模型检验、时间自动机、形式化方法

所属期刊栏目：32

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60203009,60273036;国家重点基础研究发展计划973计划2002CB31200001

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

页数：共5页

页码：193-196,213