| 题名 | 时间自动机关于LTL性质的符号化模型检测工具及其改进 |
| 作者 | 魏绪凯 |
| 学位类别 | 硕士 |
| 答辩日期 | 2009-06-04 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 中国科学院软件研究所 |
| 导师 | 李广元 |
| 中文摘要 | 许多系统需要在规定时间内响应外部发生的事件，并迅速完成对事件的处理，这样的系统称之为实时系统。实时系统经常出现在与生命财产安全息息相关的领域，如果无法及时响应外部事件，可能会造成十分严重的后果。如何保证实时系统的正确性、可靠性受到越来越广泛的关注。 模型检测是一种对系统进行形式化验证的算法，它可以自动的在模型状态空间中搜索不满足规范的路径或状态，设计者可以根据找到的反例修改系统设计，进而提高系统的可靠性。模型检测方法的主要瓶颈是状态爆炸，符号化方法和抽象是延缓状态爆炸发生的重要手段。 时间自动机是一种使用广泛的描述实时系统的数学模型， 时序逻辑LTL是是一种常用的针对实时和并发系统的规范语言，本文主要研究了时间自动机关于LTL性质的符号化模型检测方法，并实现了相应的模型检测工具CTAV。 CTAV以DBM作为表示符号化状态的数据结构，使用DBM的操作和运算完成符号化状态的生成、存储及比较等，它通过on-the-fly的方法在生成系统符号化状态空间的同时进行性质的检测。 本文还研究了最大上下界抽象等在模型检测中的使用，比较了不同的抽象在LTL模型检测中的效果。此外还针对符号化状态的特点，对模型检测过程进行了改进，避免了不必要的状态展开。 为了方便建模，CTAV对UPPAAL模型描述语言进行了支持，并针对检测过程中变量存储的各种情况，设计了一次索引和二次索引的方法提高读写变量的速度。 |
| 语种 | 中文 |
| 公开日期 | 2009-06-14 |
| 内容类型 | 学位论文 |
| 源URL | [http://124.16.136.157//handle/311060/160]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 魏绪凯. 时间自动机关于LTL性质的符号化模型检测工具及其改进[D]. 中国科学院软件研究所. 中国科学院研究生院. 2009. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论