基于整数时间的实时系统符号化模型检测技术
文献类型：学位论文
| 作者 | 晏荣杰 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-02 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 时间自动机 实时系统 模型检测 符号化方法 BDD 可达性 抽象方法 |
| 其他题名 | Integer Clock Valuation-based Symbol Model Checking Techniques for Real-time Systems |
| 中文摘要 | 实时系统是指不仅系统内部的行为及动作的完成与时间有关，而且对系统外部事件(如输入、中断等)的响应都要满足一定时间约束的系统。由于在国防及工业控制等领域应用广泛，因此这类系统的正确性及可靠性逐渐成为研究的热点。本文主要研究基于时间自动机模型的实时系统模型检测技术。 状态空间爆炸问题是制约模型检测技术实际应用的瓶颈。为了缓解状态空间爆炸问题，本文从状态集合的符号化表示方法及状态空间约简技术两个方面出发进行研究工作。 本文定义了表示状态集的符号化方法DS及SDS，用于符号化表示具有整数时钟值的状态，同时给出状态空间遍历过程中的相关算法，用于有限精度时间自动机的模型检测。 为了增强有限精度时间自动机验证过程中的数据共享程度，缩减状态空间，本文给出DS与BDD结合的方法表示状态空间，并设计了相关算法。实验结果表明这种改进方法有效的减小了状态空间遍历过程中占用的存储空间。 此外，本文还将DS与BDD结合的方法用于闭时间自动机的模型检测，提高了可验证系统的规模，并避免了单纯使用BDD记录所有离散状态时对时钟常量大小比较敏感的不足。对状态空间中状态数量及内存占用量的比较表明采用DS与BDD方法结合后的模型检测工具降低了对时钟常量的敏感程度。 在状态空间缩减方面，本文根据已有的时钟最大上下界抽象方法，给出了其在离散语义下的抽象过程，并用于DS与BDD结合的符号化模型检测过程。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 135 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7388]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 晏荣杰. 基于整数时间的实时系统符号化模型检测技术[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。