基于SPIN模型检测的电子商务协议分析与验证

发布时间：2017-09-09 11:40

  本文关键词：基于SPIN模型检测的电子商务协议分析与验证

  更多相关文章： SPIN PROMELA 模型检测 形式化方法 电子商务

【摘要】：随着互联网和分布式系统的广泛应用,电子商务的发展越来越迅速,相应的网络电子商务协议成为这种交易模式顺利进行的保证。电子商务协议的设计是一项非常庞大和复杂的工作,设计过程中极易出现意想不到的各种漏洞与缺陷,且协议在网络中呈现空间分布性、异步性和并发性等特征,这些都可能会导致不可估计的损失,因此对电子商务协议的分析与检测就成为一个现实的课题。 形式化方法是分析验证电子商务协议的一种重要方法。传统的非形式化方法很难发现协议存在的潜在问题,于是形式化分析方法就成了研究的热点。目前有许多比较著名的形式化方法如BAN逻辑、串空间模型理论、定理证明等。而模型检测方法作为形式化分析方法中的一种,能够自动验证一个系统是否满足其设计规范,具有高度自动化和提供反例等优点,可以有效减少协议设计错误,近年来被广泛应用于软硬件验证中。SPIN是其中一种著名的用于分布式系统形式化验证的模型检测工具。 本文基于模型检测工具SPIN,对HDPolyService系统中的一系列电子商务协议进行形式化分析和正确性验证。在阐述SPIN模型检测形式化分析验证机理、其建模语言PROMELA基本语法及线性时序逻辑LTL性质的基础上,详细介绍这三种“分布式”事务协议,通过分析协议设计规范提取出协议的形式化描述与状态行为转移关系,并转化为PROMELA模型作为SPIN检测工具的输入；然后根据协议模拟结果对模型进行修改完善,并采用线性时序逻辑LTL刻画出协议期望满足的属性,使用SPIN进一步检测是否满足该属性；最后根据分析和验证结果对协议设计进行完善,并总结当前工作和展望后续研究计划。验证结果表明应用SPIN对电子商务协议分析检验的可行性与普遍适用性,同时表明了这三种协议的实际应用价值。
【关键词】：SPIN PROMELA 模型检测 形式化方法 电子商务
【学位授予单位】：华东理工大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP311.52
【目录】：

• 摘要5-6
• Abstract6-9
• 第1章 绪论9-12
• 1.1 研究背景9-10
• 1.2 研究内容10-11
• 1.3 本文结构11-12
• 第2章 电子商务协议与形式化分析方法12-23
• 2.1 电子商务协议概述12-14
• 2.1.1 电子商务的定义12
• 2.1.2 电子商务协议的性质12-14
• 2.1.3 电子商务协议的分析方法简介14
• 2.2 形式化方法概述14-15
• 2.3 形式化分析方法分类15-19
• 2.3.1 信任逻辑方法15-16
• 2.3.2 定理证明方法16
• 2.3.3 模型检测方法16-19
• 2.3.4 其他通用形式方法19
• 2.4 模型检测技术19-20
• 2.4.1 模型检测方法现状19-20
• 2.4.2 模型检测与其他形式化方法的比较20
• 2.5 常见的模型检测工具20-22
• 2.6 本章小结22-23
• 第3章 协议的模型检测工具SPIN研究23-32
• 3.1 SPIN概述23-24
• 3.1.1 SPIN发展历史23
• 3.1.2 SPIN基本结构与工作原理23-24
• 3.2 SPIN模型检验理论基础24-28
• 3.2.1 线性时序逻辑LTL24-26
• 3.2.2 有限自动机26-27
• 3.2.3 SPIN基本算法27-28
• 3.3 建模语言PROMELA28-31
• 3.4 本章小结31-32
• 第4章 基于SPIN的电费代缴协议的模型检测32-53
• 4.1 协议描述33-39
• 4.1.1 HDPolyService系统33-34
• 4.1.2 协议内容34-36
• 4.1.3 电费代缴协议的说明36-39
• 4.2 电费代缴协议的形式化描述39-45
• 4.2.1 协议的PROMELA模型结构39-41
• 4.2.2 协议的主体状态与行为描述41-45
• 4.3 协议验证的属性描述45-46
• 4.4 协议行为的模拟分析46-50
• 4.5 协议属性验证结果分析50-52
• 4.6 本章小结52-53
• 第5章 支付宝定单代付协议与手机充值协议的模型检测53-67
• 5.1 支付宝定单代付协议53-59
• 5.1.1 协议内容与说明53-54
• 5.1.2 协议的形式化描述54-58
• 5.1.3 协议属性的提取与描述58-59
• 5.2 支付宝定单代付协议模拟与检测59-61
• 5.2.1 基于SPIN的协议行为模拟59-60
• 5.2.2 协议属性的验证60-61
• 5.3 手机充值协议61-64
• 5.3.1 手机充值协议描述61-62
• 5.3.2 协议的PROMELA语言描述62-64
• 5.4 协议的SPIN模拟分析与检测64-66
• 5.5 本章小结66-67
• 第6章 总结与展望67-69
• 6.1 论文总结67
• 6.2 展望67-69
• 参考文献69-72
• 致谢72

【参考文献】

中国期刊全文数据库 前10条

1 冯杰;;WTP协议的SPIN模型检测[J];电脑知识与技术;2008年34期

2 钱俊彦;赵岭忠;;基于自动机理论的符号模型检验[J];兰州理工大学学报;2008年05期

3 沈浩,孙永强;自动机与模型检查[J];计算机工程与应用;2004年01期

4 段风琴;李祥;;Petri网性质的线性时序逻辑描述与Spin检验[J];计算机科学;2006年05期

5 李彦;张文博;陈宁江;;基于模型检查实现J2EE规范的实例研究[J];计算机科学;2006年12期

6 郭建;边明明;韩俊岗;;LTL公式到自动机的转换[J];计算机科学;2008年07期

7 敬超;常亮;古天龙;;基于SPIN的无线传感器网络安全协议建模与分析[J];计算机科学;2009年10期

8 支小莉,陆鑫达,戎璐;Promela行为模型的自动抽象[J];计算机工程;2004年16期

9 黎升洪;冯艳清;;第三方支付的基于SPIN的形式化分析[J];计算机时代;2008年12期

10 黎升洪;缪淮扣;张新林;;线性时态逻辑中的特性模式[J];计算机应用;2006年08期

中国博士学位论文全文数据库 前1条

1 万良;基于行为时序逻辑TLA的系统、规则与协议检测的研究[D];贵州大学;2009年

中国硕士学位论文全文数据库 前10条

1 莫燕;网络安全协议模型检测技术研究与应用[D];西安电子科技大学;2005年

2 李文全;基于符号模型检验的电子商务协议原子性的研究与实现[D];东北大学;2005年

3 孙守卿;基于模型检测工具SPIN的安全协议分析和验证[D];兰州大学;2006年

4 王巧丽;SPIN模型检测的研究与应用[D];贵州大学;2006年

5 张振方;基于模型检验的软件分析方法研究[D];华中师范大学;2009年

6 黄谷;基于模型检查的网络协议分析与验证[D];湖南大学;2009年

7 张自强;基于自动机理论的UML模型一致性研究[D];兰州大学;2009年

8 刘俏威;SPIN模型检测的形式化分析机理研究及应用[D];南昌大学;2008年

9 冯杰;基于SPIN的协议的形式化分析和验证[D];贵州大学;2009年

10 高丹丹;无线认证协议的模型检测与分析研究[D];长春理工大学;2010年

，

本文编号：820233