中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
题名:
时间自动机关于LTL性质的符号化模型检测工具及其改进
作者: 魏绪凯
答辩日期: 2009-06-04
导师: 李广元
授予单位: 中国科学院研究生院
授予地点: 中国科学院软件研究所
学位: 硕士
摘要: 许多系统需要在规定时间内响应外部发生的事件,并迅速完成对事件的处理,这样的系统称之为实时系统。实时系统经常出现在与生命财产安全息息相关的领域,如果无法及时响应外部事件,可能会造成十分严重的后果。如何保证实时系统的正确性、可靠性受到越来越广泛的关注。 模型检测是一种对系统进行形式化验证的算法,它可以自动的在模型状态空间中搜索不满足规范的路径或状态,设计者可以根据找到的反例修改系统设计,进而提高系统的可靠性。模型检测方法的主要瓶颈是状态爆炸,符号化方法和抽象是延缓状态爆炸发生的重要手段。 时间自动机是一种使用广泛的描述实时系统的数学模型, 时序逻辑LTL是是一种常用的针对实时和并发系统的规范语言,本文主要研究了时间自动机关于LTL性质的符号化模型检测方法,并实现了相应的模型检测工具CTAV。 CTAV以DBM作为表示符号化状态的数据结构,使用DBM的操作和运算完成符号化状态的生成、存储及比较等,它通过on-the-fly的方法在生成系统符号化状态空间的同时进行性质的检测。 本文还研究了最大上下界抽象等在模型检测中的使用,比较了不同的抽象在LTL模型检测中的效果。此外还针对符号化状态的特点,对模型检测过程进行了改进,避免了不必要的状态展开。 为了方便建模,CTAV对UPPAAL模型描述语言进行了支持,并针对检测过程中变量存储的各种情况,设计了一次索引和二次索引的方法提高读写变量的速度。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/160
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
魏绪凯 毕业论文ex.pdf(869KB)----限制开放 联系获取全文

Recommended Citation:
魏绪凯. 时间自动机关于LTL性质的符号化模型检测工具及其改进[D]. 中国科学院软件研究所. 中国科学院研究生院. 2009-06-04.
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