Institutional Repository
| 卫命令模型检测工具的设计与实现 | |
| 王绍春 | |
| Major | 计算机软件与理论 |
| Supervisor | 张文辉 |
| 2010-06-03 | |
| Degree Grantor | 中国科学院研究生院 |
| Degree Level | 硕士 |
| Place of Degree Grantor | 北京 |
| Keyword | 模型检测，卫命令，线性时序逻辑，自动机，偏序规约，双深度优先搜索，时序滤网 |
| English Abstract | 计算机软硬件系统日益复杂，可靠性的保证变得日益困难。传统的测试方 法在处理并发系统时效果欠佳，人们需要更可靠的方法来保证系统的正确性。 模型检测技术应运而生。 模型检测技术是一种基于有穷状态空间的自动验证技术，相对于定理证明 它具有更高的自动化程度。模型检测技术目前已广泛应用到协议分析、电路设 计等各个方面，各种模型检测工具也应运而生。 本文描述了一个以卫命令为模型描述语言，以线性时序逻辑为性质指定语 言的模型检测工具的设计与实现。主要内容包括自动机的模型检测方法，双深 度优先搜索算法，偏序规约等方法的实现。本文提出了一个改进的双深度优先 搜索算法，我们称之为多交错双深度优先算法。另外，关于偏序规约，我们探 讨了它在卫命令系统中的具体实现方法。本文还讨论了有限串上的线性时序逻 辑在网络分析中的应用，提出了时序滤网的概念，并用它分析了一些网络安全 问题。 |
| Subject | 计算机科学技术基础学科 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/2331 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 王绍春. 卫命令模型检测工具的设计与实现[D]. 北京. 中国科学院研究生院,2010. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| thesis.pdf（659KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment