中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于整数时间的实时系统符号化模型检测技术
作者: 晏荣杰
答辩日期: 2007-06-02
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 时间自动机 ; 实时系统 ; 模型检测 ; 符号化方法 ; BDD ; 可达性 ; 抽象方法
其他题名: Integer Clock Valuation-based Symbol Model Checking Techniques for Real-time Systems
摘要: 实时系统是指不仅系统内部的行为及动作的完成与时间有关,而且对系统外部事件(如输入、中断等)的响应都要满足一定时间约束的系统。由于在国防及工业控制等领域应用广泛,因此这类系统的正确性及可靠性逐渐成为研究的热点。本文主要研究基于时间自动机模型的实时系统模型检测技术。 状态空间爆炸问题是制约模型检测技术实际应用的瓶颈。为了缓解状态空间爆炸问题,本文从状态集合的符号化表示方法及状态空间约简技术两个方面出发进行研究工作。 本文定义了表示状态集的符号化方法DS及SDS,用于符号化表示具有整数时钟值的状态,同时给出状态空间遍历过程中的相关算法,用于有限精度时间自动机的模型检测。 为了增强有限精度时间自动机验证过程中的数据共享程度,缩减状态空间,本文给出DS与BDD结合的方法表示状态空间,并设计了相关算法。实验结果表明这种改进方法有效的减小了状态空间遍历过程中占用的存储空间。 此外,本文还将DS与BDD结合的方法用于闭时间自动机的模型检测,提高了可验证系统的规模,并避免了单纯使用BDD记录所有离散状态时对时钟常量大小比较敏感的不足。对状态空间中状态数量及内存占用量的比较表明采用DS与BDD方法结合后的模型检测工具降低了对时钟常量的敏感程度。 在状态空间缩减方面,本文根据已有的时钟最大上下界抽象方法,给出了其在离散语义下的抽象过程,并用于DS与BDD结合的符号化模型检测过程。
英文摘要: In real time systems, not only the behavior and actions have the strong connection with time, but also the response to the environment should satisfy certain constraints on clock valuations. It is widely applied to industrial and military applications, with the high requirement for the correctness and reliability. The paper focuses on the model checking techniques, based on the formal modeling of the real time systems by timed automata. State explosion is a bottleneck which limits the scale of the verified system and real applications. To relieve the state explosion problem, the thesis is devoted to two aspects of research: the symbolic representation of reachable configurations and the methods of state space reduction. Two symbolic methods DS and SDS are defined to record the reachable configurations for integer clock valuations. Meanwhile the related algorithms for reachability analysis are discussed in detail. To improve the data sharing ability and reduce the memory occupation for finite precision timed automata, the combined representation of DS and BDD is proposed, as well as the algorithms for reachability analysis. The experiments show the improvement on memory reduction. Besides the application of symbolic methods for finite precision timed automata, the symbolic representation for closed timed automata is also applied. The combination of symbolic methods and data sharing enhances the scale of verified system, and decreases the sensitivity to the domain of clock constants. Location based maximal lower and upper bounds is applied to the abstraction for integer clock valuations and integrated into the combined symbolic representation of DS and BDD. The method enhances the performance of state space reduction.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7388
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200318015001003晏荣杰_paper.pdf(1648KB)----限制开放-- 联系获取全文

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