| 基于模型检测的多轮FR协议验证 |
| |
| 引用本文： | 郭华,庄雷,张习勇,李舟军. 基于模型检测的多轮FR协议验证[J]. 计算机科学, 2008, 35(5): 95-98 |
| |
| 作者姓名： | 郭华 庄雷 张习勇 李舟军 |
| |
| 作者单位： | 北京航空航天大学计算机学院,北京,100083;郑州大学理论计算机研究所,郑州,450052;解放军信息工程大学,郑州,450002 |
| |
| 基金项目： | 国家自然科学基金 , 河南省教育厅基础研究项目 |
| |
| 摘 要： | 随着网络的大规模应用,越来越多的协议在并发环境中执行,时间也成为协议中一个重要因素.本文对公平交换协议Franklin/Reiter协议加入了时间因素,用时间自动机对其建模,并用自动验证工具UPPAAL验证了单轮协议的性质.重点验证了并发环境中多轮协议的执行情况,最后给出了协议在多轮情况下正常执行需满足的条件.
|
| 关 键 词： | 电子商务协议 模型检测 时间自动机 UPPAAL 多轮执行 |
Verifying Multiple Runs of FR Protocol Using Model Checking |
| |
| GUO Hua,ZHUANG Lei,ZHANG Xi-yong,LI Zhou-jun. Verifying Multiple Runs of FR Protocol Using Model Checking[J]. Computer Science, 2008, 35(5): 95-98 |
| |
| Authors: | GUO Hua ZHUANG Lei ZHANG Xi-yong LI Zhou-jun |
| |
| Affiliation: | GUO Hua~1 ZHUANG Lei~2 ZHANG Xi-yong~3 LI Zhou-jun~1 (School of Computer Science & Engineering,Beihang University,Beijing 100083,China)~1(Institute of Information Engineering,Zhengzhou University,Zhengzhou 450052,China)~2(Institute of Information Engineering,Information Engineering University,Zhengzhou 450002,China)~3 |
| |
| Abstract: | With the growing popularity of the Internet,more and more protocols run concurrently.In this paper,time is added to the FR protocol,and timed automata is used to model Franklin/Reiter protocol.Then UPPAAL is used to verify some properties of the protocol.This paper focuses on multiple runs of FR protocol,and gives some qualifica- tions ensuring that the protocol runs successfully in the concurrent environment. |
| |
| Keywords: | E-commerce protocol Formal verification Timed automata UPPAAL Multiple runs |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
