| Netbill协议原子性的符号模型检验分析 |
| |
| 引用本文： | 郭云川,古天龙,董荣胜,蔡国永.Netbill协议原子性的符号模型检验分析[J].计算机工程与应用,2004,40(2):57-59. |
| |
| 作者姓名： | 郭云川 古天龙 董荣胜 蔡国永 |
| |
| 作者单位： | 桂林电子工业学院计算机系,桂林,541004 |
| |
| 基金项目： | 广西跨世纪人才基金项目，广西科学基金项目(编号:0141046)资助 |
| |
| 摘 要： | 电子商务协议的安全性和原子性是电子商务研究者和使用者广泛关心的问题,采取一定的方法对协议进行分析检验是协议开发过程中一个必要环节。论文在对Netbill协议及其原子性进行形式化描述的基础上,基于符号模型检验器(SMV)从钱原子性和商品原子性两个角度对Netbill协议进行了分析和检验,从而表明了用SMV对电子商务协议分析和验证的可行性。
|
| 关 键 词： | 电子商务协议 符号模型检验 原子性 |
| 文章编号： | 1002-8331-(2004)02-0057-03 |
Symbolic Model Checking Analysis for Atomicity of Netbill Protocol |
| |
| Guo Yunchuan Gu,Tianlong Dong Rongsheng Cai,Guoyong.Symbolic Model Checking Analysis for Atomicity of Netbill Protocol[J].Computer Engineering and Applications,2004,40(2):57-59. |
| |
| Authors: | Guo Yunchuan Gu Tianlong Dong Rongsheng Cai Guoyong |
| |
| Abstract: | In e-commerce field,security and atomicity of e-commerce protocols are two important issues.It is a neces-sary step to analyze and verify them in the developing protocol.In this paper,the Netbill protocol and its atomicity are formally represented.Then the atomicity of money and goods is analyzed and verified using symbolic model verifier(SMV).It is shown that SMV is a suitable tool to analyze and verify e-commerce protocols. |
| |
| Keywords: | Electronic Commerce Protocol Symbolic Model Checking Atomicity |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
