离散时间自动机模型检测工具的设计与实现
文献类型：学位论文
| 作者 | 张文亮 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-02 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 实时系统 可达性 二叉判定图 非空性 模型检测 |
| 中文摘要 | 模型检测是一种自动完成性质验证的算法过程，模型检测器是模型检测算法的工具实现，可用来检验系统是否满足某些性质，如可达性、安全性等，可以及时发现问题，更改系统设计中的缺陷，避免不必要的损失。实时系统由于涉及并发、不确定性以及时间约束等因素，其设计的正确性很难把握，因此利用模型检测对其进行分析显得更为重要。 CTAV/Reach是一个基于离散时间自动机的实时系统模型检测工具，利用它可以对可达性、安全性等性质进行检测。实验表明该工具具有良好的检测效率。 本文给出了CTAV/Reach的设计框架，重点介绍了可达性检测算法的设计与实现，以及实现过程中采用的一些优化策略，包括活动时钟约减技术、LU抽象方法等，并研究对比了各种策略对检测效率的影响，实验表明这些优化策略明显加快了检测速度。CTAV/Reach的状态空间用二叉判定图实现，文中研究对比了不同的变量序对状态空间大小的影响。通过与另一个模型检测工具Rabbit的比较体现了CTAV/Reach对时钟常量取值的敏感度较低的特点。 本文还介绍了一个基于离散时间自动机的非空性检测工具CTAV/LTL，利用它可以进行LTL性质的检测。文中主要介绍了CTAV/LTL的状态空间展开算法与使用的数据结构，并与其它检测工具进行了实验比较，说明了CTAV/LTL良好的检测效率。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 76 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7430]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 张文亮. 离散时间自动机模型检测工具的设计与实现[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。