|
|||||
|
|
| 基于模型检测的多轮FR协议验证 | |
| 作者姓名： | 郭华 庄雷 张习勇 李舟军 |
| 作者单位： | 北京航空航天大学计算机学院,北京,100083;郑州大学理论计算机研究所,郑州,450052;解放军信息工程大学,郑州,450002 |
| 基金项目： | 国家自然科学基金 , 河南省教育厅基础研究项目 |
| 摘 要： | 随着网络的大规模应用,越来越多的协议在并发环境中执行,时间也成为协议中一个重要因素.本文对公平交换协议Franklin/Reiter协议加入了时间因素,用时间自动机对其建模,并用自动验证工具UPPAAL验证了单轮协议的性质.重点验证了并发环境中多轮协议的执行情况,最后给出了协议在多轮情况下正常执行需满足的条件. |
| 关 键 词： | 电子商务协议 模型检测 时间自动机 UPPAAL 多轮执行 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |