会议专题

基于UPPAAL的简单网络支付协议形式化验证

  本文分析了简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息。在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷。新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境。

时间自动机 电子商务协议 UPPAAL 原子性

余兴超 马争先 王玉斌 董荣胜

桂林电子科技大学计算机科学与工程学院,广西桂林 541004

国内会议

广西计算机学会2010年年会

南宁

中文

465-468

2010-09-01(万方平台首次上网日期,不代表论文的发表时间)