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