摘要
为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略。采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题。与DTSp in等著名的模型检测工具进行了实验比较,取得了较好的实验结果。
The research on model checking based on timed automata is done in order to enhance the model checking tool＇ s ability and efficiency. The process of the state - space＇ s generation is further analyzed. The design and implementation of the model checking tool that cheeks LTL properties is well studied, and the results of different strategies are discussed. Some improvements of the generation and storage of the state - space are made to enhance the model checking tool＇ s ability and efficiency. A data structure named BDD（ Binary Decision Diagram） is used to reduce the consumption of memory in the process of state - space generation. The experimental results show that this tool is more effective than other similar tools, such as the famous DTSpin.
出处
《计算机仿真》
CSCD
北大核心
2009年第5期92-95,共4页
Computer Simulation
基金
国家自然科学基金(60673051,60736017,60721061)
国家973计划资助(2002cb312200)
