首页--工业技术论文--自动化技术、计算机技术论文--计算技术、计算机技术论文--计算机软件论文--程序设计、软件工程论文--软件工程论文

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

摘要第1-6页
Abstract第6-9页
第1章 绪论第9-12页
   ·研究背景第9-10页
   ·研究内容第10-11页
   ·本文结构第11-12页
第2章 电子商务协议与形式化分析方法第12-23页
   ·电子商务协议概述第12-14页
     ·电子商务的定义第12页
     ·电子商务协议的性质第12-14页
     ·电子商务协议的分析方法简介第14页
   ·形式化方法概述第14-15页
   ·形式化分析方法分类第15-19页
     ·信任逻辑方法第15-16页
     ·定理证明方法第16页
     ·模型检测方法第16-19页
     ·其他通用形式方法第19页
   ·模型检测技术第19-20页
     ·模型检测方法现状第19-20页
     ·模型检测与其他形式化方法的比较第20页
   ·常见的模型检测工具第20-22页
   ·本章小结第22-23页
第3章 协议的模型检测工具SPIN研究第23-32页
   ·SPIN概述第23-24页
     ·SPIN发展历史第23页
     ·SPIN基本结构与工作原理第23-24页
   ·SPIN模型检验理论基础第24-28页
     ·线性时序逻辑LTL第24-26页
     ·有限自动机第26-27页
     ·SPIN基本算法第27-28页
   ·建模语言PROMELA第28-31页
   ·本章小结第31-32页
第4章 基于SPIN的电费代缴协议的模型检测第32-53页
   ·协议描述第33-39页
     ·HDPolyService系统第33-34页
     ·协议内容第34-36页
     ·电费代缴协议的说明第36-39页
   ·电费代缴协议的形式化描述第39-45页
     ·协议的PROMELA模型结构第39-41页
     ·协议的主体状态与行为描述第41-45页
   ·协议验证的属性描述第45-46页
   ·协议行为的模拟分析第46-50页
   ·协议属性验证结果分析第50-52页
   ·本章小结第52-53页
第5章 支付宝定单代付协议与手机充值协议的模型检测第53-67页
   ·支付宝定单代付协议第53-59页
     ·协议内容与说明第53-54页
     ·协议的形式化描述第54-58页
     ·协议属性的提取与描述第58-59页
   ·支付宝定单代付协议模拟与检测第59-61页
     ·基于SPIN的协议行为模拟第59-60页
     ·协议属性的验证第60-61页
   ·手机充值协议第61-64页
     ·手机充值协议描述第61-62页
     ·协议的PROMELA语言描述第62-64页
   ·协议的SPIN模拟分析与检测第64-66页
   ·本章小结第66-67页
第6章 总结与展望第67-69页
   ·论文总结第67页
   ·展望第67-69页
参考文献第69-72页
致谢第72页

论文共72页,点击 下载论文
上一篇:基于能力成熟度模型的信息系统安全保障评估
下一篇:空间路径聚类算法的建模与研究