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

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

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

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