中国科学院软件研究所机构知识库
Advanced  
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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7430
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200428015029135张文亮_paper.doc(1996KB)----限制开放-- 联系获取全文

Recommended Citation:
张文亮. 离散时间自动机模型检测工具的设计与实现[D]. 软件研究所. 中国科学院软件研究所. 2007-06-02.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[张文亮]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[张文亮]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace