QQ客服 官方微博 反馈留言

题名	带时间约束的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模型描述语言中函数成分的支持，以及模型检测完成后反例的输出，方便用户对模型的修改和完善。
语种	中文
学科主题	计算机科学技术基础学科 ; 自动机理论
公开日期	2010-06-08
内容类型	学位论文
源URL	[http://124.16.136.157/handle/311060/2335]
专题	软件研究所_计算机科学国家重点实验室 _学位论文
推荐引用方式 GB/T 7714	部德振. 带时间约束的LTL公式的模型检测技术及工具实现[D]. 北京. 中国科学院研究生院. 2010.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。