| 不可靠环境下多轮FR协议分析 |
| |
| 引用本文： | 郭华,庄雷,张习勇.不可靠环境下多轮FR协议分析[J].计算机工程与应用,2006,42(33):142-145. |
| |
| 作者姓名： | 郭华 庄雷 张习勇 |
| |
| 作者单位： | 1. 郑州大学,理论计算机研究所,郑州,450052
2. 郑州大学,数学系,郑州,450052 |
| |
| 基金项目： | 国家自然科学基金;河南省教育厅基础研究项目 |
| |
| 摘 要： | 随着网络的大规模应用,越来越多的协议在并发的、不可靠的环境中执行。文章用有限自动机对FR协议建模,并用自动验证工具UPPAAL验证了多轮协议在可靠环境下的性质。重点验证了不可靠环境中多轮协议的执行情况,最后对协议进行了修改。
|
| 关 键 词： | 电子商务协议 模型检测 不可靠环境 多轮执行 UPPAAL |
| 文章编号： | 1002-8331（2006）33-0142-04 |
| 收稿时间： | 2006-02 |
| 修稿时间： | 2006-02 |
Failure Analysis of Multiple Runs of FR Protocol Using Model Checking |
| |
| GUO Hua,ZHUANG Lei,ZHANG Xi-yong.Failure Analysis of Multiple Runs of FR Protocol Using Model Checking[J].Computer Engineering and Applications,2006,42(33):142-145. |
| |
| Authors: | GUO Hua ZHUANG Lei ZHANG Xi-yong |
| |
| Affiliation: | l.Institute of Information Engineering,Zhengzhou University,Zhengzhou 450052, China; 2.Department of Mathematics,Zhengzhou University,Zhengzhou 450052, China |
| |
| Abstract: | With the growing popularity of the lnternet,more and more protocols run concurrently.In this paper,finite state automata is used to model FR protocol.Then UPPAAL is used to verify some properties of the protocol when the site or communication is reliable.Thls paper focuses on multiple runs of FR protocol in the presence of site or comunication failure. |
| |
| Keywords: | UPPAAL |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
