| 时间自动机的LTL性质模型检测研究 |
| |
| 引用本文： | 彭云全,魏绪凯,李广元.时间自动机的LTL性质模型检测研究[J].计算机仿真,2009,26(5). |
| |
| 作者姓名： | 彭云全 魏绪凯 李广元 |
| |
| 作者单位： | 1. 中国科学院软件研究所,北京,100080;中国科学院研究生院,北京,100049
2. 中国科学院软件研究所,北京,100080 |
| |
| 基金项目： | 国家自然科学基金，国家重点基础研究发展规划(973计划) |
| |
| 摘 要： | 为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.
|
| 关 键 词： | 时间自动机 模型检测 线性时序逻辑性质 二叉决策图共享存储 |
LTL Model Checking for Timed Automata |
| |
| PENG Yun-quan,WEI Xu-kai,LI Guang-yuan.LTL Model Checking for Timed Automata[J].Computer Simulation,2009,26(5). |
| |
| Authors: | PENG Yun-quan WEI Xu-kai LI Guang-yuan |
| |
| Affiliation: | 1.Institute o Software;Chinese Academy of Sciences;Beijing 100080;China;2.Graduate School;Beijing 100049;China |
| |
| Abstract: | 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 checks 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... |
| |
| Keywords: | Timed automata Model checking LTL property Binary decision diagram |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
