计算机科学 ›› 2008, Vol. 35 ›› Issue (5): 95-98.
• • 上一篇 下一篇
出版日期:
发布日期:
基金资助:
Online:
Published:
摘要： 随着网络的大规模应用，越来越多的协议在并发环境中执行，时间也成为协议中一个重要因素。本文对公平交换协议Franklin／Reiter协议加入了时间因素，用时间自动机对其建模，并用自动验证工具UPPAAL验证了单轮协议的性质。重点验证了并发环境中多轮协议的执行情况，最后给出了协议在多轮情况下正常执行需满足的条件。
关键词: 电子商务协议 模型检测 时间自动机 UPPAAL 多轮执行
Abstract: With the growing popularity of the Internet, more and more protocols run concurrently. In this paper, time is added to the FR protocol, and timed automata is used to model Franklin/Reiter protocol. Then UPPAAL is used to verify some properties of the prot
Key words: E-commerce protocol, Formal verification, Timed automata, UPPAAL, Multiple runs
. 基于模型检测的多轮FR协议验证[J]. 计算机科学, 2008, 35(5): 95-98. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2008/V35/I5/95
Cited
首页