中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机软件
题名:
基于Yices对时间自动机的有界模型检测
作者: 王晓亮
答辩日期: 2009-06-05
导师: 张文辉
授予单位: 中科院软件所
授予地点: 中科院软件所
学位: 硕士
关键词: 有界模型检测,时间自动机,SMT工具,可达性,安全性,逻辑公式
其他题名: Bounded Model Checking for Timed Automata Based on Yices
摘要: 随着工业化程度的提高,对模型的检测方法受到越来越大的重视。通常的检测方法有推理验证和模型检测。而相对于推理验证,模型检测由于其高度自动化的检测过程,在工业界有着更广泛的应用。 模型检测自从概念雏形开始之时,就受到状态爆炸问题的困扰。为了解决这个问题,不同的技术被提了出来。McMillan提出利用OBDD的符号模型检测方法在一定程度上解决了这个问题。另外,本文所主要讲述的有界模型检测,经大量的实践证明,对符号模型检测也是一个很好的补充。 由于问题的特殊性,科学家提出来不同的模型来描述不同情况的系统。由于时间自动机能够很好地描述异步系统,而且这种系统广泛地存在于现实生活中,对时间自动机这种特殊模型的验证方法的研究变得很有必要。另外,由于时间自动机带有实数域的时钟变量,这导致了时间自动机有一个无限域的状态迁移图。为了利用模型检测的方法对其进行验证,需要对时间变量进行预处理。一般的方法是把时钟所对应的时钟区或时钟域根据等价性,化为有限的域,相应地,把时间自动机转化为有限的状态迁移图。 为了避免在对时间自动机有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,本文给出一个利用SMT工具进行的对时间自动机进行有界模型检测的方法。该方法的主要优点是无需将时间自动机中的时钟进行预处理,也不需要将模型中的变量进行布尔编码,只需将时间自动机转变为SMT工具可解的逻辑公式,利用SMT的高效求解来进行模型检测。实验结果表明,对于某些可达性性质的验证,这种方法的效率有一定的优势。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/105
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200628015029029王晓亮_paper.pdf(880KB)----限制开放 联系获取全文

Recommended Citation:
王晓亮. 基于Yices对时间自动机的有界模型检测[D]. 中科院软件所. 中科院软件所. 2009-06-05.
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