广西科学院学报
廣西科學院學報
엄서과학원학보
JOURNAL OF GUANGXI ACADEMY OF SCIENCES
2010年
4期
465-468
,共4页
余兴超%马争先%王玉斌%董荣胜
餘興超%馬爭先%王玉斌%董榮勝
여흥초%마쟁선%왕옥빈%동영성
时间自动机%电子商务协议%UPPAAL%原子性
時間自動機%電子商務協議%UPPAAL%原子性
시간자동궤%전자상무협의%UPPAAL%원자성
分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用 UPPAAL工具验证其是否满足商品原子性.新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息,在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷.新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境.
分析簡單支付協議中不同銀行間的交易行為和各主體的超時約束,建立消費者、商傢、銀行和超時計時器的時間自動機模型,併用 UPPAAL工具驗證其是否滿足商品原子性.新模型在原模型的基礎上,增加瞭超時計時器進程來負責接收來自其它進程的超時信息,在各主體的計時器觸髮超時之後,計時器將髮送超時信息,再通過外部的仲裁程序來解決糾紛.新模型能夠滿足貨幣原子性和商品原子性,併且比原模型更加符閤協議運行的實際環境.
분석간단지부협의중불동은행간적교역행위화각주체적초시약속,건립소비자、상가、은행화초시계시기적시간자동궤모형,병용 UPPAAL공구험증기시부만족상품원자성.신모형재원모형적기출상,증가료초시계시기진정래부책접수래자기타진정적초시신식,재각주체적계시기촉발초시지후,계시기장발송초시신식,재통과외부적중재정서래해결규분.신모형능구만족화폐원자성화상품원자성,병차비원모형경가부합협의운행적실제배경.
