Institutional Repository
| 实时系统非空性模型检测工具及技术 | |
| 彭云全 | |
| 2008-05-28 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 软件研究所 |
| Keyword | 实时系统 二叉判定图 非空性 模型检测 |
| English Abstract | 实时系统是指能及时响应外部发生的事件，并以足够快的速度完成对事件处理的计算机应用系统。实时系统应用的场合往往要求其正确性和可靠性能够得到保证，但是由于涉及并发、不确定性以及时间约束等因素，实时系统设计的正确性很难把握。为了确保实时系统的正确性和可靠性，发现系统设计中可能存在的缺陷，利用模型检测技术和工具对其进行分析检测是十分重要的。 时间自动机是实时系统常用的一种形式化模型，LTL是一种常用的时序逻辑语言。本文将介绍实时系统的一个基于时间自动机模型的LTL性质检测工具CTAV。本文介绍了CTAV的设计框架，重点介绍了对CTAV中LTL性质检测过程的优化和改进，对比研究了各种优化策略对检测效率和检测能力的影响。这些优化策略包括改进时间自动机复合的计算生成过程、引入BDD利用BDD的数据共享降低检测过程的空间消耗、把一些状态空间削减的优化方案引入非空性模型检测、利用编码压缩技术减少状态存储占用的内存空间。实验结果表明这些优化策略改进了CTAV的检测能力。 本文还介绍了时间自动机基于BDD表示的符号化LTL性质检测的一些研究工作。主要介绍了用BDD表示时间约束、状态迁移等以及通过BDD操作来完成后继状态的生成。 |
| Pages | 89 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/5824 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 彭云全. 实时系统非空性模型检测工具及技术[D]. 软件研究所. 中国科学院软件研究所,2008. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 10001_20052801502900（746KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment