离散时间自动机模型检测工具的设计与实现

ISCAS OpenIR > 中科院软件所 > 中科院软件所

	离散时间自动机模型检测工具的设计与实现
	张文亮
	2007-06-02
学位授予单位	中国科学院软件研究所
学位	博士
学位授予地点	软件研究所
关键词	实时系统可达性二叉判定图非空性模型检测
摘要	模型检测是一种自动完成性质验证的算法过程，模型检测器是模型检测算法的工具实现，可用来检验系统是否满足某些性质，如可达性、安全性等，可以及时发现问题，更改系统设计中的缺陷，避免不必要的损失。实时系统由于涉及并发、不确定性以及时间约束等因素，其设计的正确性很难把握，因此利用模型检测对其进行分析显得更为重要。 CTAV/Reach是一个基于离散时间自动机的实时系统模型检测工具，利用它可以对可达性、安全性等性质进行检测。实验表明该工具具有良好的检测效率。本文给出了CTAV/Reach的设计框架，重点介绍了可达性检测算法的设计与实现，以及实现过程中采用的一些优化策略，包括活动时钟约减技术、LU抽象方法等，并研究对比了各种策略对检测效率的影响，实验表明这些优化策略明显加快了检测速度。CTAV/Reach的状态空间用二叉判定图实现，文中研究对比了不同的变量序对状态空间大小的影响。通过与另一个模型检测工具Rabbit的比较体现了CTAV/Reach对时钟常量取值的敏感度较低的特点。本文还介绍了一个基于离散时间自动机的非空性检测工具CTAV/LTL，利用它可以进行LTL性质的检测。文中主要介绍了CTAV/LTL的状态空间展开算法与使用的数据结构，并与其它检测工具进行了实验比较，说明了CTAV/LTL良好的检测效率。
其他摘要	Model checking is an automatic technique for verifying finite state systems. Model checker is the implementation of the model checking algorithms, which can be used to check whether some given properties, such as reachability, safety, are satisfied in the system. Using model checker we can find the errors in the system. Compared to untimed systems, real-time systems are more complicated because of their additional timing constraints. It’s very difficult to confirm the correctness of the real-time system’s design, so it’s important to verify and analyze real-time systems using model checking tools. CTAV/Reach is a model checker based on discrete timed automata, which is aimed to verify the reachability of real-time systems.This paper presents the design and implementation of CTAV/Reach, especially the reachability analysis algorithm and the data structures used in the algorithm. This paper also discusses some strategies used to optimize the performance of the checker, such as active clock reduction, LU abstract method and so on.Experiment shows that CTAV/Reach is less sensitive to clock constants value than Rabbit, another model checker for real-time systems. Another model checker called CTAV/LTL, based on discrete timed automata, is also introduced in this paper. CTAV/LTL can verify linear temporal logic (LTL) properties for closed timed automata. Compared to other model checkers which can check LTL properties for real-time systems, CTAV/LTL has good performance.
页数	76
语种	中文
内容类型	学位论文
URI标识	http://ir.iscas.ac.cn/handle/311060/7430
专题	中科院软件所_中科院软件所
推荐引用方式 GB/T 7714	张文亮. 离散时间自动机模型检测工具的设计与实现[D]. 软件研究所. 中国科学院软件研究所,2007.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
10001_20042801502913（1996KB）			限制开放	--	请求全文