基于ATL的形式化建模與驗(yàn)證技術(shù)的應(yīng)用研究.pdf

1、本文基于形式化方法，結(jié)合ATL（Alternating-time Temporal Logic）對(duì)形式化建模與驗(yàn)證技術(shù)的應(yīng)用進(jìn)行了研究，研究領(lǐng)域主要集中在應(yīng)用廣泛的公平交換協(xié)議和前景廣闊的微電網(wǎng)電源管理系統(tǒng)方面。
　　本文基于ATL及其拓展語(yǔ)言rPATL做了兩個(gè)工作，第一個(gè)工作結(jié)合ATL及MOCHA工具對(duì)公平交換協(xié)議中廣泛應(yīng)用的電子合同簽署協(xié)議進(jìn)行形式化建模與系統(tǒng)規(guī)格描述，并驗(yàn)證其是否滿足公平性、及時(shí)性和不可濫用性。本文通過(guò)對(duì)MO

2、CHA工具的驗(yàn)證結(jié)果進(jìn)行分析，發(fā)現(xiàn)本文選用的電子合同簽署協(xié)議不滿足公平性、及時(shí)性與不可濫用性，存在一定的缺陷，不符合設(shè)計(jì)需求；第二個(gè)工作結(jié)合rPATL及PRISM-games工具對(duì)復(fù)雜的、帶有概率變遷的微電網(wǎng)電源管理系統(tǒng)進(jìn)行建模，模擬復(fù)雜的微電網(wǎng)電源管理系統(tǒng)中帶有概率的狀態(tài)遷移與執(zhí)行過(guò)程，并計(jì)算出微電網(wǎng)中的各個(gè)分布式供電電源在一定時(shí)間內(nèi)所提供的電能及消耗的燃料。
　　本文把形式化方法應(yīng)用在使用十分廣泛的公平交換協(xié)議中，對(duì)公平交換協(xié)

3、議的公平性、及時(shí)性和不可濫用性進(jìn)行了嚴(yán)謹(jǐn)?shù)拿枋龊陀行У尿?yàn)證，不僅發(fā)現(xiàn)了其潛在的漏洞，還分析出其問(wèn)題所在，能夠有效的幫助協(xié)議的設(shè)計(jì)者對(duì)協(xié)議進(jìn)行改進(jìn)。此外，本文還創(chuàng)新性的把形式化方法應(yīng)用到新興的微電網(wǎng)技術(shù)中，把復(fù)雜的微電網(wǎng)電源管理系統(tǒng)抽象化描述成一個(gè)十分簡(jiǎn)單的帶有概率的多玩家游戲系統(tǒng)，然后對(duì)微電網(wǎng)的電源管理系統(tǒng)進(jìn)行形式化建模，并模擬計(jì)算出微電網(wǎng)各個(gè)分布式電源在一定時(shí)間內(nèi)所能提供的電能與消耗的燃料，對(duì)微電網(wǎng)的實(shí)際部署工作具有一定的參考意義。<