中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机科学技术基础学科 ; 计算机科学技术基础学科::自动机理论
题名:
带时间约束的LTL公式的模型检测技术及工具实现
作者: 部德振
答辩日期: 2010-06-03
导师: 李广元
专业: 计算机软件与理论
授予单位: 中国科学院研究生院
授予地点: 北京
学位: 硕士
关键词: 实时系统 ; 时间自动机 ; 时间约束 ; LTL性质 ; 模型检测
摘要: 实时系统是能够在指定或确定的时间内完成事件处理的计算机应用系统,它的正确性不仅依赖于系统计算的逻辑结果,还依赖于产生这个结果的时间。实时系统在国防以及工业控制等领域的到广泛应用,为保证系统的正确性和可靠性,使用模型检测方法对其进行检测十分重要。 时间自动机是对实时系统进行建模的一种形式化方法,线性时序逻辑(LTL)是当前常用的描述性质的时序逻辑。CTAV是国际上目前唯一的可对时间自动机直接进行线性时序逻辑性质验证的符号化模型检测工具,但CTAV还不能直接检测带时间约束的线性时序逻辑性质,如果要检测带时间约束的线性时序逻辑性质,需要使用者通过手动构造test时间自动机来实现,这增加了使用者的困难。 为了验证时间自动机M是否满足一个带时间约束的线性时序逻辑q, 本文首先在LTL公式转化Büchi自动机的基础上给出了将带时间约束的LTL公式q转化为时间Büchi自动机Bq的方法,其次针对由性质转化而来的时间Büchi自动机Bq(性质自动机)的特点,本文给出了一个构造乘积自动机M*Bq的过程,使得可将验证M是否满足的问题化归为乘积自动机M*Bq的空性检测问题,由于乘积自动机M*Bq是一个时间Büchi自动机,这样通过调用CTAV中以前已实现的关于时间Büchi自动机的空性检测过程就得到了带时间约束的线性时序逻辑关于时间自动机的一个模型检测过程。此外还修改了LU的计算过程,最后给出了实验数据对比,得到了一个比较好的实现方法。 本文还完善了CTAV对UPPAL模型描述语言中函数成分的支持,以及模型检测完成后反例的输出,方便用户对模型的修改和完善。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/2335
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
部德振-毕业论文.pdf(455KB)----限制开放 联系获取全文

Recommended Citation:
部德振. 带时间约束的LTL公式的模型检测技术及工具实现[D]. 北京. 中国科学院研究生院. 2010-06-03.
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