| 卫命令模型检测工具的设计与实现 |
| 王绍春
|
| 专业 | 计算机软件与理论
|
| 导师 | 张文辉
|
| 2010-06-03
|
| 学位授予单位 | 中国科学院研究生院
|
| 学位 | 硕士
|
| 学位授予地点 | 北京
|
| 关键词 | 模型检测，卫命令，线性时序逻辑，自动机，偏序规约，双深度优先搜索，时序滤网
|
| 摘要 | 计算机软硬件系统日益复杂，可靠性的保证变得日益困难。传统的测试方
法在处理并发系统时效果欠佳，人们需要更可靠的方法来保证系统的正确性。
模型检测技术应运而生。
模型检测技术是一种基于有穷状态空间的自动验证技术，相对于定理证明
它具有更高的自动化程度。模型检测技术目前已广泛应用到协议分析、电路设
计等各个方面，各种模型检测工具也应运而生。
本文描述了一个以卫命令为模型描述语言，以线性时序逻辑为性质指定语
言的模型检测工具的设计与实现。主要内容包括自动机的模型检测方法，双深
度优先搜索算法，偏序规约等方法的实现。本文提出了一个改进的双深度优先
搜索算法，我们称之为多交错双深度优先算法。另外，关于偏序规约，我们探
讨了它在卫命令系统中的具体实现方法。本文还讨论了有限串上的线性时序逻
辑在网络分析中的应用，提出了时序滤网的概念，并用它分析了一些网络安全
问题。 |
| 学科领域 | 计算机科学技术基础学科
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/2331
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
王绍春. 卫命令模型检测工具的设计与实现[D]. 北京. 中国科学院研究生院,2010.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论