| WTP协议的SPIN模型检测 |
| |
| 引用本文： | 冯杰.WTP协议的SPIN模型检测[J].数字社区&智能家居,2008,3(12):1588-1591. |
| |
| 作者姓名： | 冯杰 |
| |
| 作者单位： | 贵州大学电子科学与信息技术学院,贵州贵阳550025 |
| |
| 摘 要： | 基于模型检测技术，使用SPIN对WTP协议进行了建模和分析．应用自动机和Promela对协议进行建模。利用LTL规范了协议需要满足的安全性，时序性。通过分析发现了协议的一个错误。
|
| 关 键 词： | WTP协议 SPIN 模型检测 Promela |
Model Checking of WTP Protocol Via SPIN |
| |
| FENG Jie.Model Checking of WTP Protocol Via SPIN[J].Digital Community & Smart Home,2008,3(12):1588-1591. |
| |
| Authors: | FENG Jie |
| |
| Affiliation: | FENG Jie (Electronic Science and Information Technology College, Guizhou University, Guiyang 550025, China) |
| |
| Abstract: | This paper deals with a formal verification of WTP, where the model checking approach is applied by SPIN model checker.The Promela model is developed and LTL specifications of secrecy are given. Eventually, some defects has been revealed. |
| |
| Keywords: | WTP Protocol SPIN model checking Promela |
| 本文献已被 维普 等数据库收录！ |
