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