Institutional Repository
| 带时间约束的LTL公式的模型检测技术及工具实现 | |
| 部德振 | |
| Major | 计算机软件与理论 |
| Supervisor | 李广元 |
| 2010-06-03 | |
| Degree Grantor | 中国科学院研究生院 |
| Degree Level | 硕士 |
| Place of Degree Grantor | 北京 |
| Keyword | 实时系统 时间自动机 时间约束 Ltl性质 模型检测 |
| English Abstract | 实时系统是能够在指定或确定的时间内完成事件处理的计算机应用系统，它的正确性不仅依赖于系统计算的逻辑结果，还依赖于产生这个结果的时间。实时系统在国防以及工业控制等领域的到广泛应用，为保证系统的正确性和可靠性，使用模型检测方法对其进行检测十分重要。 时间自动机是对实时系统进行建模的一种形式化方法，线性时序逻辑（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模型描述语言中函数成分的支持，以及模型检测完成后反例的输出，方便用户对模型的修改和完善。 |
| Subject | 计算机科学技术基础学科 ; 自动机理论 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/2335 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 部德振. 带时间约束的LTL公式的模型检测技术及工具实现[D]. 北京. 中国科学院研究生院,2010. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 部德振-毕业论文.pdf（455KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment