| 引用本文： |
-
余兴超,马争先,王玉斌,董荣胜.基于UPPAAL的简单网络支付协议形式化验证[J].广西科学院学报,2010,26(4):465-468. [点击复制]
- YU Xing-chao,MA Zheng-xian,WANG Yu-bin,DONG Rong-sheng.Formal Verification of SNPP Based on UPPAAL[J].Journal of Guangxi Academy of Sciences,2010,26(4):465-468. [点击复制]
|
|
| 摘要: |
| 分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息,在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷。新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境。 |
| 关键词: 时间自动机 电子商务协议 UPPAAL 原子性 |
| DOI： |
| 投稿时间：2010-08-06修订日期：2010-08-21 |
| 基金项目:广西自然科学基金项目(桂科自0991242)资助。 |
|
| Formal Verification of SNPP Based on UPPAAL |
|
YU Xing-chao, MA Zheng-xian, WANG Yu-bin, DONG Rong-sheng
|
| (School of Computer Science and Engineering, Guilin University of Electronic Technology, Guilin, Guangxi, 541004, China) |
| Abstract: |
| The transaction actions between different banks and the overtime of main bodies in Simple Network Payment Protocol are analyzed.The timed automata models of customer, merchant, banks and overtime timer are established. UPPAAL is used to verify the satisfication of protocol with goods atomicity. The new model,based on the original one, adds overtime timer to receive the overtime informations from other processes and sends out overtime messages after overtime timer of each main bodies are triggered.Then the issue is solved by external arbitration procedure. The new model satisfies money and goods atomicity, and is more suitable than the original for the protocol in realistic environment. |
| Key words: timed automata e-commerce protocol UPPAAL atomicity |
