电子商务协议原子性的SPIN分析  

SPIN Analysis for Atomicity of Electronic Commerce Protocols

作　　者：王兵[1] 肖美华[1] 刘晓清[1] 朱宜炳[1] 

机构地区：[1]南昌大学计算中心,江西南昌330031

出　　处：《南昌大学学报（工科版）》2007年第2期181-185,共5页Journal of Nanchang University(Engineering & Technology)

基　　金：国家重大基础研究973计划前期预研项目(2003CCA02800);江西省自然科学基金资助项目(0411041;0611057);江西省教育厅2005年科技计划资助项目(200543)

摘　　要：电子商务协议的研究有利于促进电子商务的发展,电子商务协议的原子性是电子商务协议研究的重点.对NetBill协议及其原子性在开放性的环境中进行形式化描述的基础上,给出基于SPIN平台的NetBill协议模型,用LTL刻画协议需要满足的性质,用模型检测器SPIN对NetBill协议分析结果表明NetBill协议满足原子性.该方法对类似电子商务协议的其它性质分析具有一定的通用性.The research of electronic commerce protocols may be used to improve electronic commerce. The atomicity of electronic commerce protocols is important in the research of electronic commerce protocols. Based on formal description for the NetBill protocol and its atomicity in complex environments, a NetBill protocol＇ s model is presented using SPIN platform and the protocol properties are specified by LTL. The experiment result shows that the NetBill protocol meets the atomicity. The method is universal to analyze the other proporties of similar protocols.

关 键 词：电子商务协议 SPIN 原子性 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]