基于ATL的形式化建模与验证技术的应用研究

发布时间：2017-06-12 23:06

  本文关键词：基于ATL的形式化建模与验证技术的应用研究，由笔耕文化传播整理发布。

【摘要】：本文基于形式化方法,结合ATL(Alternating-time Temporal Logic)对形式化建模与验证技术的应用进行了研究,研究领域主要集中在应用广泛的公平交换协议和前景广阔的微电网电源管理系统方面。本文基于ATL及其拓展语言rPATL做了两个工作,第一个工作结合ATL及MOCHA工具对公平交换协议中广泛应用的电子合同签署协议进行形式化建模与系统规格描述,并验证其是否满足公平性、及时性和不可滥用性。本文通过对MOCHA工具的验证结果进行分析,发现本文选用的电子合同签署协议不满足公平性、及时性与不可滥用性,存在一定的缺陷,不符合设计需求;第二个工作结合rPATL及PRISM-games工具对复杂的、带有概率变迁的微电网电源管理系统进行建模,模拟复杂的微电网电源管理系统中带有概率的状态迁移与执行过程,并计算出微电网中的各个分布式供电电源在一定时间内所提供的电能及消耗的燃料。本文把形式化方法应用在使用十分广泛的公平交换协议中,对公平交换协议的公平性、及时性和不可滥用性进行了严谨的描述和有效的验证,不仅发现了其潜在的漏洞,还分析出其问题所在,能够有效的帮助协议的设计者对协议进行改进。此外,本文还创新性的把形式化方法应用到新兴的微电网技术中,把复杂的微电网电源管理系统抽象化描述成一个十分简单的带有概率的多玩家游戏系统,然后对微电网的电源管理系统进行形式化建模,并模拟计算出微电网各个分布式电源在一定时间内所能提供的电能与消耗的燃料,对微电网的实际部署工作具有一定的参考意义。本文基于游戏理论的思想,把复杂的系统抽象描述成一个简单的游戏系统,是一种十分自然且易于理解的描述方式,在简单的游戏系统上进行建模和验证也能够帮助我们纵览整个系统,摒弃系统中不重要的细节部分,对我们关注的关键部分进行形式化分析与验证。此外,本文采用的形式化验证方法是一种高度抽象的验证方法,能够对复杂的系统进行有效的分析与验证,同时,也能够灵活、有效的拓展到其他领域的系统建模与验证中。
【关键词】：ATL rPATL 形式化验证 模型检测 电子合同签署协议 微电网
【学位授予单位】：暨南大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TM743
【目录】：

• 摘要3-4
• Abstract4-7
• 第一章 绪论7-13
• 1.1 本文研究背景7-9
• 1.2 本文研究内容9
• 1.3 国内外的研究现状9-11
• 1.4 本文研究意义11
• 1.5 本文结构11-13
• 第二章 背景知识13-18
• 2.1 公平交换协议简介13-15
• 2.2 微电网简介15-18
• 第三章 时态逻辑语言与形式化验证工具18-27
• 3.1 ATL与MOCHA工具18-22
• 3.2 rPATL与PRISM-games工具22-27
• 第四章 系统的形式化建模与规格描述27-42
• 4.1 公平交换协议的形式化建模与规格描述27-34
• 4.2 微电网电源管理系统的形式化建模与规格描述34-42
• 第五章 形式化验证结果与分析42-47
• 5.1 公平交换协议的验证结果与分析42-44
• 5.2 微电网的计算结果与分析44-47
• 第六章 工作总结与展望47-48
• 参考文献48-53
• 附录53-65
• 已发表的论文65-66
• 致谢66

【相似文献】

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

1 马忠贵;叶斌;曾广平;涂序彦;;基于π演算的软件人群体形式化建模[J];北京理工大学学报;2006年02期

2 田旭光;朱元昌;邸彦强;;指挥与控制系统复杂网络形式化建模与分析[J];电光与控制;2012年07期

3 王世进;;分布式制造调度体系结构的π演算形式化建模[J];计算机工程与应用;2010年09期

4 赵庶旭;王小龙;;CTCS-3行车许可过程形式化建模[J];计算机工程与设计;2013年06期

5 孔莹莹;蒲海涛;隋瑞升;;基于CPN的UML2.0形式化建模[J];青岛大学学报(工程技术版);2011年01期

6 ;[J];;年期

中国重要会议论文全文数据库 前1条

1 蔡远利;于振华;王瑞峰;;多Agent系统形式化建模方法学[A];'2006系统仿真技术及其应用学术交流会论文集[C];2006年

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

1 陈永;基于高可信无线通信的列车流形式化建模与仿真[D];兰州交通大学;2014年

2 胡晓辉;智能分布监控系统软件形式化建模和设计研究[D];西北工业大学;2007年

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

1 李群;基于ATL的形式化建模与验证技术的应用研究[D];暨南大学;2016年

2 吕增威;矿井机车无人驾驶系统无线区段交接过程形式化建模与验证研究[D];合肥工业大学;2015年

3 夏倩倩;协同应用流程并行交互的形式化建模研究[D];内蒙古大学;2012年

4 肖知屹;列车安全距离控制形式化建模与验证[D];兰州交通大学;2014年

5 熊锡娇;列车自动防护系统的形式化建模与验证方法研究[D];华东师范大学;2012年

6 李丹;λ噬菌体生活周期的形式化建模与分析[D];上海交通大学;2007年

7 刘密霞;基于策略的信息安全模型及形式化建模的研究[D];兰州理工大学;2004年

8 周佳铭;基于PVS对SCADE开发轨交控制系统的形式化建模与验证[D];华东师范大学;2011年

9 濮阳;生物过程的形式化建模及仿真[D];上海交通大学;2007年

10 杨蒙;HMIPv6协议形式化建模及测试例生成方法研究[D];内蒙古大学;2010年

  本文关键词：基于ATL的形式化建模与验证技术的应用研究，，由笔耕文化传播整理发布。

本文编号：445135