本文關(guān)鍵詞：基于ATL的形式化建模與驗(yàn)證技術(shù)的應(yīng)用研究，由筆耕文化傳播整理發(fā)布。

【摘要】：本文基于形式化方法,結(jié)合ATL(Alternating-time Temporal Logic)對形式化建模與驗(yàn)證技術(shù)的應(yīng)用進(jìn)行了研究,研究領(lǐng)域主要集中在應(yīng)用廣泛的公平交換協(xié)議和前景廣闊的微電網(wǎng)電源管理系統(tǒng)方面。本文基于ATL及其拓展語言rPATL做了兩個(gè)工作,第一個(gè)工作結(jié)合ATL及MOCHA工具對公平交換協(xié)議中廣泛應(yīng)用的電子合同簽署協(xié)議進(jìn)行形式化建模與系統(tǒng)規(guī)格描述,并驗(yàn)證其是否滿足公平性、及時(shí)性和不可濫用性。本文通過對MOCHA工具的驗(yàn)證結(jié)果進(jìn)行分析,發(fā)現(xiàn)本文選用的電子合同簽署協(xié)議不滿足公平性、及時(shí)性與不可濫用性,存在一定的缺陷,不符合設(shè)計(jì)需求;第二個(gè)工作結(jié)合rPATL及PRISM-games工具對復(fù)雜的、帶有概率變遷的微電網(wǎng)電源管理系統(tǒng)進(jìn)行建模,模擬復(fù)雜的微電網(wǎng)電源管理系統(tǒng)中帶有概率的狀態(tài)遷移與執(zhí)行過程,并計(jì)算出微電網(wǎng)中的各個(gè)分布式供電電源在一定時(shí)間內(nèi)所提供的電能及消耗的燃料。本文把形式化方法應(yīng)用在使用十分廣泛的公平交換協(xié)議中,對公平交換協(xié)議的公平性、及時(shí)性和不可濫用性進(jìn)行了嚴(yán)謹(jǐn)?shù)拿枋龊陀行У尿?yàn)證,不僅發(fā)現(xiàn)了其潛在的漏洞,還分析出其問題所在,能夠有效的幫助協(xié)議的設(shè)計(jì)者對協(xié)議進(jìn)行改進(jìn)。此外,本文還創(chuàng)新性的把形式化方法應(yīng)用到新興的微電網(wǎng)技術(shù)中,把復(fù)雜的微電網(wǎng)電源管理系統(tǒng)抽象化描述成一個(gè)十分簡單的帶有概率的多玩家游戲系統(tǒng),然后對微電網(wǎng)的電源管理系統(tǒng)進(jìn)行形式化建模,并模擬計(jì)算出微電網(wǎng)各個(gè)分布式電源在一定時(shí)間內(nèi)所能提供的電能與消耗的燃料,對微電網(wǎng)的實(shí)際部署工作具有一定的參考意義。本文基于游戲理論的思想,把復(fù)雜的系統(tǒng)抽象描述成一個(gè)簡單的游戲系統(tǒng),是一種十分自然且易于理解的描述方式,在簡單的游戲系統(tǒng)上進(jìn)行建模和驗(yàn)證也能夠幫助我們縱覽整個(gè)系統(tǒng),摒棄系統(tǒng)中不重要的細(xì)節(jié)部分,對我們關(guān)注的關(guān)鍵部分進(jìn)行形式化分析與驗(yàn)證。此外,本文采用的形式化驗(yàn)證方法是一種高度抽象的驗(yàn)證方法,能夠?qū)?fù)雜的系統(tǒng)進(jìn)行有效的分析與驗(yàn)證,同時(shí),也能夠靈活、有效的拓展到其他領(lǐng)域的系統(tǒng)建模與驗(yàn)證中。
【關(guān)鍵詞】：ATL rPATL 形式化驗(yàn)證 模型檢測 電子合同簽署協(xié)議 微電網(wǎng)
【學(xué)位授予單位】：暨南大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TM743
【目錄】：

• 摘要3-4
• Abstract4-7
• 第一章 緒論7-13
• 1.1 本文研究背景7-9
• 1.2 本文研究內(nèi)容9
• 1.3 國內(nèi)外的研究現(xiàn)狀9-11
• 1.4 本文研究意義11
• 1.5 本文結(jié)構(gòu)11-13
• 第二章 背景知識13-18
• 2.1 公平交換協(xié)議簡介13-15
• 2.2 微電網(wǎng)簡介15-18
• 第三章 時(shí)態(tài)邏輯語言與形式化驗(yàn)證工具18-27
• 3.1 ATL與MOCHA工具18-22
• 3.2 rPATL與PRISM-games工具22-27
• 第四章 系統(tǒng)的形式化建模與規(guī)格描述27-42
• 4.1 公平交換協(xié)議的形式化建模與規(guī)格描述27-34
• 4.2 微電網(wǎng)電源管理系統(tǒng)的形式化建模與規(guī)格描述34-42
• 第五章 形式化驗(yàn)證結(jié)果與分析42-47
• 5.1 公平交換協(xié)議的驗(yàn)證結(jié)果與分析42-44
• 5.2 微電網(wǎng)的計(jì)算結(jié)果與分析44-47
• 第六章 工作總結(jié)與展望47-48
• 參考文獻(xiàn)48-53
• 附錄53-65
• 已發(fā)表的論文65-66
• 致謝66

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前6條

1 馬忠貴;葉斌;曾廣平;涂序彥;;基于π演算的軟件人群體形式化建模[J];北京理工大學(xué)學(xué)報(bào);2006年02期

2 田旭光;朱元昌;邸彥強(qiáng);;指揮與控制系統(tǒng)復(fù)雜網(wǎng)絡(luò)形式化建模與分析[J];電光與控制;2012年07期

3 王世進(jìn);;分布式制造調(diào)度體系結(jié)構(gòu)的π演算形式化建模[J];計(jì)算機(jī)工程與應(yīng)用;2010年09期

4 趙庶旭;王小龍;;CTCS-3行車許可過程形式化建模[J];計(jì)算機(jī)工程與設(shè)計(jì);2013年06期

5 孔瑩瑩;蒲海濤;隋瑞升;;基于CPN的UML2.0形式化建模[J];青島大學(xué)學(xué)報(bào)(工程技術(shù)版);2011年01期

6 ;[J];;年期

中國重要會議論文全文數(shù)據(jù)庫 前1條

1 蔡遠(yuǎn)利;于振華;王瑞峰;;多Agent系統(tǒng)形式化建模方法學(xué)[A];'2006系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)交流會論文集[C];2006年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前2條

1 陳永;基于高可信無線通信的列車流形式化建模與仿真[D];蘭州交通大學(xué);2014年

2 胡曉輝;智能分布監(jiān)控系統(tǒng)軟件形式化建模和設(shè)計(jì)研究[D];西北工業(yè)大學(xué);2007年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 李群;基于ATL的形式化建模與驗(yàn)證技術(shù)的應(yīng)用研究[D];暨南大學(xué);2016年

2 呂增威;礦井機(jī)車無人駕駛系統(tǒng)無線區(qū)段交接過程形式化建模與驗(yàn)證研究[D];合肥工業(yè)大學(xué);2015年

3 夏倩倩;協(xié)同應(yīng)用流程并行交互的形式化建模研究[D];內(nèi)蒙古大學(xué);2012年

4 肖知屹;列車安全距離控制形式化建模與驗(yàn)證[D];蘭州交通大學(xué);2014年

5 熊錫嬌;列車自動防護(hù)系統(tǒng)的形式化建模與驗(yàn)證方法研究[D];華東師范大學(xué);2012年

6 李丹;λ噬菌體生活周期的形式化建模與分析[D];上海交通大學(xué);2007年

7 劉密霞;基于策略的信息安全模型及形式化建模的研究[D];蘭州理工大學(xué);2004年

8 周佳銘;基于PVS對SCADE開發(fā)軌交控制系統(tǒng)的形式化建模與驗(yàn)證[D];華東師范大學(xué);2011年

9 濮陽;生物過程的形式化建模及仿真[D];上海交通大學(xué);2007年

10 楊蒙;HMIPv6協(xié)議形式化建模及測試?yán)煞椒ㄑ芯縖D];內(nèi)蒙古大學(xué);2010年

  本文關(guān)鍵詞：基于ATL的形式化建模與驗(yàn)證技術(shù)的應(yīng)用研究，，由筆耕文化傳播整理發(fā)布。

本文編號：445135