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

• 作者: 余兴超 王玉斌 董荣胜 马争先
• 来源期刊: 广西科学院学报
• 学科: 工学
• 关键词: 时间自动机 电子商务协议 UPPAAL 原子性
• 年，卷（期）: 2010,（4）
• 页码范围: 465-468
• 分类号: TP301.1
• 字数: 3647字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-7378.2010.04.024

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董荣胜	桂林电子科技大学计算机科学与工程学院	115	1521	13.0	37.0
2	马争先	桂林电子科技大学计算机科学与工程学院	4	6	2.0	2.0
3	王玉斌	桂林电子科技大学计算机科学与工程学院	6	12	2.0	2.0
4	余兴超	桂林电子科技大学计算机科学与工程学院	6	8	2.0	2.0