一种电子商务协议原子性的模型检验分析方法  

Model Checking Analysis for Atomicity of Electronic Commerce Protocol

作　　者：董荣胜[1] 郭云川[1] 古天龙[1] 

机构地区：[1]桂林电子工业学院计算机系,桂林541004

出　　处：《计算机科学》2005年第4期184-186,共3页Computer Science

基　　金：广西自然科学基金项目(桂科字0229051)的资助

摘　　要：提出了一个分析电子商务协议的形式化模型,介绍了基于该模型的电子商务协议原子性的描述方法。同其他模型相比,该模型能较好地分析具有多个实例并发运行时电子商务协议的原子性。最后基于该模型,用符号模型检验工具(SMV)分析了Digicash协议和Netbill协议。A simple model for modeling electronic commerce protocol is proposed and a novel technique for formally describing its atomicity is presented. The model can be used to analyze atomicity and adapted to meet the situation that more than one instances of protocols run concurrently. Taking the protocols Digicash and Netbill as the exam- ples, the paper presents the method how to implement the model based on the symbolic model verifier-SMV.

关 键 词：电子商务协议 原子性 检验分析 形式化模型 描述方法 检验工具 符号模型 

分 类 号：TP309[自动化与计算机技术—计算机系统结构] TP311.13[自动化与计算机技术—计算机科学与技术]