中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
实时系统非空性模型检测工具及技术
作者: 彭云全
答辩日期: 2008-05-28
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 实时系统 ; 二叉判定图 ; 非空性 ; 模型检测
摘要: 实时系统是指能及时响应外部发生的事件,并以足够快的速度完成对事件处理的计算机应用系统。实时系统应用的场合往往要求其正确性和可靠性能够得到保证,但是由于涉及并发、不确定性以及时间约束等因素,实时系统设计的正确性很难把握。为了确保实时系统的正确性和可靠性,发现系统设计中可能存在的缺陷,利用模型检测技术和工具对其进行分析检测是十分重要的。 时间自动机是实时系统常用的一种形式化模型,LTL是一种常用的时序逻辑语言。本文将介绍实时系统的一个基于时间自动机模型的LTL性质检测工具CTAV。本文介绍了CTAV的设计框架,重点介绍了对CTAV中LTL性质检测过程的优化和改进,对比研究了各种优化策略对检测效率和检测能力的影响。这些优化策略包括改进时间自动机复合的计算生成过程、引入BDD利用BDD的数据共享降低检测过程的空间消耗、把一些状态空间削减的优化方案引入非空性模型检测、利用编码压缩技术减少状态存储占用的内存空间。实验结果表明这些优化策略改进了CTAV的检测能力。 本文还介绍了时间自动机基于BDD表示的符号化LTL性质检测的一些研究工作。主要介绍了用BDD表示时间约束、状态迁移等以及通过BDD操作来完成后继状态的生成。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5824
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200528015029002彭云全_paper.pdf(746KB)----限制开放-- 联系获取全文

Recommended Citation:
彭云全. 实时系统非空性模型检测工具及技术[D]. 软件研究所. 中国科学院软件研究所. 2008-05-28.
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