实时系统非空性模型检测工具及技术
文献类型：学位论文
| 作者 | 彭云全 |
| 学位类别 | 博士 |
| 答辩日期 | 2008-05-28 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 实时系统 二叉判定图 非空性 模型检测 |
| 中文摘要 | 实时系统是指能及时响应外部发生的事件，并以足够快的速度完成对事件处理的计算机应用系统。实时系统应用的场合往往要求其正确性和可靠性能够得到保证，但是由于涉及并发、不确定性以及时间约束等因素，实时系统设计的正确性很难把握。为了确保实时系统的正确性和可靠性，发现系统设计中可能存在的缺陷，利用模型检测技术和工具对其进行分析检测是十分重要的。 时间自动机是实时系统常用的一种形式化模型，LTL是一种常用的时序逻辑语言。本文将介绍实时系统的一个基于时间自动机模型的LTL性质检测工具CTAV。本文介绍了CTAV的设计框架，重点介绍了对CTAV中LTL性质检测过程的优化和改进，对比研究了各种优化策略对检测效率和检测能力的影响。这些优化策略包括改进时间自动机复合的计算生成过程、引入BDD利用BDD的数据共享降低检测过程的空间消耗、把一些状态空间削减的优化方案引入非空性模型检测、利用编码压缩技术减少状态存储占用的内存空间。实验结果表明这些优化策略改进了CTAV的检测能力。 本文还介绍了时间自动机基于BDD表示的符号化LTL性质检测的一些研究工作。主要介绍了用BDD表示时间约束、状态迁移等以及通过BDD操作来完成后继状态的生成。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 89 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5824]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 彭云全. 实时系统非空性模型检测工具及技术[D]. 软件研究所. 中国科学院软件研究所. 2008. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。