| 乐观合同签订协议的模型检测分析 |
| |
| 引用本文： | 周立青,杨晋吉. 乐观合同签订协议的模型检测分析[J]. 计算机工程, 2011, 37(7): 142-144,147. DOI: 10.3969/j.issn.1000-3428.2011.07.047 |
| |
| 作者姓名： | 周立青 杨晋吉 |
| |
| 作者单位： | 华南师范大学计算机学院,广州,510631 |
| |
| 基金项目： | 国家"973"计划基金资助项目，广东省科技计划基金资助项目 |
| |
| 摘 要： | 从ECS1协议和PFH协议出发，研究三轮乐观合同签订协议的结构。利用协议动作序列及条件图建立协议模型，分析三轮协议满足有限性的条件。在此基础上，结合模型检测工具SPIN，对满足有限性的协议结构的公平性进行分析、验证，并给出反例，说明三轮协议不可能同时满足有限性和公平性。
|
| 关 键 词： | 合同签订协议 乐观 模型检测 公平性 有限性 |
Model Checking Analysis of Optimistic Contract Signing Protocol |
| |
| ZHOU Li-qing,YANG Jin-ji. Model Checking Analysis of Optimistic Contract Signing Protocol[J]. Computer Engineering, 2011, 37(7): 142-144,147. DOI: 10.3969/j.issn.1000-3428.2011.07.047 |
| |
| Authors: | ZHOU Li-qing YANG Jin-ji |
| |
| Affiliation: | (School of Computer,South China Normal University,Guangzhou 510631,China) |
| |
| Abstract: | This paper studies the various structures of three-round optimistic contract signing protocol.The protocol structures are modeled by protocol motion chart and the property of timeliness is analyzed.Getting the structures which meet the timeliness requirement,it further analyzes and verifies the fairness property.Counterexamples are given by the model checker SPIN.Result shows that three-round protocols can not achieve both the fairness and timeliness. |
| |
| Keywords: | contract signing protocol optimistic model checking fairness timeliness |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
