%0 Journal Article
%T 基于模型检测的多轮fr协议验证
%J 计算机科学
%D 2008
%X 随着网络的大规模应用，越来越多的协议在并发环境中执行，时间也成为协议中一个重要因素。本文对公平交换协议franklin／reiter协议加入了时间因素，用时间自动机对其建模，并用自动验证工具uppaal验证了单轮协议的性质。重点验证了并发环境中多轮协议的执行情况，最后给出了协议在多轮情况下正常执行需满足的条件。
%K 电子商务协议模型检测时间自动机uppaal多轮执行
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=27274614&flag=1