本文關(guān)鍵詞：基于SPIN模型檢測(cè)的電子商務(wù)協(xié)議分析與驗(yàn)證

  更多相關(guān)文章： SPIN PROMELA 模型檢測(cè) 形式化方法 電子商務(wù)

【摘要】：隨著互聯(lián)網(wǎng)和分布式系統(tǒng)的廣泛應(yīng)用,電子商務(wù)的發(fā)展越來(lái)越迅速,相應(yīng)的網(wǎng)絡(luò)電子商務(wù)協(xié)議成為這種交易模式順利進(jìn)行的保證。電子商務(wù)協(xié)議的設(shè)計(jì)是一項(xiàng)非常龐大和復(fù)雜的工作,設(shè)計(jì)過(guò)程中極易出現(xiàn)意想不到的各種漏洞與缺陷,且協(xié)議在網(wǎng)絡(luò)中呈現(xiàn)空間分布性、異步性和并發(fā)性等特征,這些都可能會(huì)導(dǎo)致不可估計(jì)的損失,因此對(duì)電子商務(wù)協(xié)議的分析與檢測(cè)就成為一個(gè)現(xiàn)實(shí)的課題。 形式化方法是分析驗(yàn)證電子商務(wù)協(xié)議的一種重要方法。傳統(tǒng)的非形式化方法很難發(fā)現(xiàn)協(xié)議存在的潛在問(wèn)題,于是形式化分析方法就成了研究的熱點(diǎn)。目前有許多比較著名的形式化方法如BAN邏輯、串空間模型理論、定理證明等。而模型檢測(cè)方法作為形式化分析方法中的一種,能夠自動(dòng)驗(yàn)證一個(gè)系統(tǒng)是否滿足其設(shè)計(jì)規(guī)范,具有高度自動(dòng)化和提供反例等優(yōu)點(diǎn),可以有效減少協(xié)議設(shè)計(jì)錯(cuò)誤,近年來(lái)被廣泛應(yīng)用于軟硬件驗(yàn)證中。SPIN是其中一種著名的用于分布式系統(tǒng)形式化驗(yàn)證的模型檢測(cè)工具。 本文基于模型檢測(cè)工具SPIN,對(duì)HDPolyService系統(tǒng)中的一系列電子商務(wù)協(xié)議進(jìn)行形式化分析和正確性驗(yàn)證。在闡述SPIN模型檢測(cè)形式化分析驗(yàn)證機(jī)理、其建模語(yǔ)言PROMELA基本語(yǔ)法及線性時(shí)序邏輯LTL性質(zhì)的基礎(chǔ)上,詳細(xì)介紹這三種“分布式”事務(wù)協(xié)議,通過(guò)分析協(xié)議設(shè)計(jì)規(guī)范提取出協(xié)議的形式化描述與狀態(tài)行為轉(zhuǎn)移關(guān)系,并轉(zhuǎn)化為PROMELA模型作為SPIN檢測(cè)工具的輸入；然后根據(jù)協(xié)議模擬結(jié)果對(duì)模型進(jìn)行修改完善,并采用線性時(shí)序邏輯LTL刻畫(huà)出協(xié)議期望滿足的屬性,使用SPIN進(jìn)一步檢測(cè)是否滿足該屬性；最后根據(jù)分析和驗(yàn)證結(jié)果對(duì)協(xié)議設(shè)計(jì)進(jìn)行完善,并總結(jié)當(dāng)前工作和展望后續(xù)研究計(jì)劃。驗(yàn)證結(jié)果表明應(yīng)用SPIN對(duì)電子商務(wù)協(xié)議分析檢驗(yàn)的可行性與普遍適用性,同時(shí)表明了這三種協(xié)議的實(shí)際應(yīng)用價(jià)值。
【關(guān)鍵詞】：SPIN PROMELA 模型檢測(cè) 形式化方法 電子商務(wù)
【學(xué)位授予單位】：華東理工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2012
【分類號(hào)】：TP311.52
【目錄】：

• 摘要5-6
• Abstract6-9
• 第1章 緒論9-12
• 1.1 研究背景9-10
• 1.2 研究?jī)?nèi)容10-11
• 1.3 本文結(jié)構(gòu)11-12
• 第2章 電子商務(wù)協(xié)議與形式化分析方法12-23
• 2.1 電子商務(wù)協(xié)議概述12-14
• 2.1.1 電子商務(wù)的定義12
• 2.1.2 電子商務(wù)協(xié)議的性質(zhì)12-14
• 2.1.3 電子商務(wù)協(xié)議的分析方法簡(jiǎn)介14
• 2.2 形式化方法概述14-15
• 2.3 形式化分析方法分類15-19
• 2.3.1 信任邏輯方法15-16
• 2.3.2 定理證明方法16
• 2.3.3 模型檢測(cè)方法16-19
• 2.3.4 其他通用形式方法19
• 2.4 模型檢測(cè)技術(shù)19-20
• 2.4.1 模型檢測(cè)方法現(xiàn)狀19-20
• 2.4.2 模型檢測(cè)與其他形式化方法的比較20
• 2.5 常見(jiàn)的模型檢測(cè)工具20-22
• 2.6 本章小結(jié)22-23
• 第3章 協(xié)議的模型檢測(cè)工具SPIN研究23-32
• 3.1 SPIN概述23-24
• 3.1.1 SPIN發(fā)展歷史23
• 3.1.2 SPIN基本結(jié)構(gòu)與工作原理23-24
• 3.2 SPIN模型檢驗(yàn)理論基礎(chǔ)24-28
• 3.2.1 線性時(shí)序邏輯LTL24-26
• 3.2.2 有限自動(dòng)機(jī)26-27
• 3.2.3 SPIN基本算法27-28
• 3.3 建模語(yǔ)言PROMELA28-31
• 3.4 本章小結(jié)31-32
• 第4章 基于SPIN的電費(fèi)代繳協(xié)議的模型檢測(cè)32-53
• 4.1 協(xié)議描述33-39
• 4.1.1 HDPolyService系統(tǒng)33-34
• 4.1.2 協(xié)議內(nèi)容34-36
• 4.1.3 電費(fèi)代繳協(xié)議的說(shuō)明36-39
• 4.2 電費(fèi)代繳協(xié)議的形式化描述39-45
• 4.2.1 協(xié)議的PROMELA模型結(jié)構(gòu)39-41
• 4.2.2 協(xié)議的主體狀態(tài)與行為描述41-45
• 4.3 協(xié)議驗(yàn)證的屬性描述45-46
• 4.4 協(xié)議行為的模擬分析46-50
• 4.5 協(xié)議屬性驗(yàn)證結(jié)果分析50-52
• 4.6 本章小結(jié)52-53
• 第5章 支付寶定單代付協(xié)議與手機(jī)充值協(xié)議的模型檢測(cè)53-67
• 5.1 支付寶定單代付協(xié)議53-59
• 5.1.1 協(xié)議內(nèi)容與說(shuō)明53-54
• 5.1.2 協(xié)議的形式化描述54-58
• 5.1.3 協(xié)議屬性的提取與描述58-59
• 5.2 支付寶定單代付協(xié)議模擬與檢測(cè)59-61
• 5.2.1 基于SPIN的協(xié)議行為模擬59-60
• 5.2.2 協(xié)議屬性的驗(yàn)證60-61
• 5.3 手機(jī)充值協(xié)議61-64
• 5.3.1 手機(jī)充值協(xié)議描述61-62
• 5.3.2 協(xié)議的PROMELA語(yǔ)言描述62-64
• 5.4 協(xié)議的SPIN模擬分析與檢測(cè)64-66
• 5.5 本章小結(jié)66-67
• 第6章 總結(jié)與展望67-69
• 6.1 論文總結(jié)67
• 6.2 展望67-69
• 參考文獻(xiàn)69-72
• 致謝72

【參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 馮杰;;WTP協(xié)議的SPIN模型檢測(cè)[J];電腦知識(shí)與技術(shù);2008年34期

2 錢(qián)俊彥;趙嶺忠;;基于自動(dòng)機(jī)理論的符號(hào)模型檢驗(yàn)[J];蘭州理工大學(xué)學(xué)報(bào);2008年05期

3 沈浩,孫永強(qiáng);自動(dòng)機(jī)與模型檢查[J];計(jì)算機(jī)工程與應(yīng)用;2004年01期

4 段風(fēng)琴;李祥;;Petri網(wǎng)性質(zhì)的線性時(shí)序邏輯描述與Spin檢驗(yàn)[J];計(jì)算機(jī)科學(xué);2006年05期

5 李彥;張文博;陳寧江;;基于模型檢查實(shí)現(xiàn)J2EE規(guī)范的實(shí)例研究[J];計(jì)算機(jī)科學(xué);2006年12期

6 郭建;邊明明;韓俊崗;;LTL公式到自動(dòng)機(jī)的轉(zhuǎn)換[J];計(jì)算機(jī)科學(xué);2008年07期

7 敬超;常亮;古天龍;;基于SPIN的無(wú)線傳感器網(wǎng)絡(luò)安全協(xié)議建模與分析[J];計(jì)算機(jī)科學(xué);2009年10期

8 支小莉,陸鑫達(dá),戎璐;Promela行為模型的自動(dòng)抽象[J];計(jì)算機(jī)工程;2004年16期

9 黎升洪;馮艷清;;第三方支付的基于SPIN的形式化分析[J];計(jì)算機(jī)時(shí)代;2008年12期

10 黎升洪;繆淮扣;張新林;;線性時(shí)態(tài)邏輯中的特性模式[J];計(jì)算機(jī)應(yīng)用;2006年08期

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

1 萬(wàn)良;基于行為時(shí)序邏輯TLA的系統(tǒng)、規(guī)則與協(xié)議檢測(cè)的研究[D];貴州大學(xué);2009年

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

1 莫燕;網(wǎng)絡(luò)安全協(xié)議模型檢測(cè)技術(shù)研究與應(yīng)用[D];西安電子科技大學(xué);2005年

2 李文全;基于符號(hào)模型檢驗(yàn)的電子商務(wù)協(xié)議原子性的研究與實(shí)現(xiàn)[D];東北大學(xué);2005年

3 孫守卿;基于模型檢測(cè)工具SPIN的安全協(xié)議分析和驗(yàn)證[D];蘭州大學(xué);2006年

4 王巧麗;SPIN模型檢測(cè)的研究與應(yīng)用[D];貴州大學(xué);2006年

5 張振方;基于模型檢驗(yàn)的軟件分析方法研究[D];華中師范大學(xué);2009年

6 黃谷;基于模型檢查的網(wǎng)絡(luò)協(xié)議分析與驗(yàn)證[D];湖南大學(xué);2009年

7 張自強(qiáng);基于自動(dòng)機(jī)理論的UML模型一致性研究[D];蘭州大學(xué);2009年

8 劉俏威;SPIN模型檢測(cè)的形式化分析機(jī)理研究及應(yīng)用[D];南昌大學(xué);2008年

9 馮杰;基于SPIN的協(xié)議的形式化分析和驗(yàn)證[D];貴州大學(xué);2009年

10 高丹丹;無(wú)線認(rèn)證協(xié)議的模型檢測(cè)與分析研究[D];長(zhǎng)春理工大學(xué);2010年

，

本文編號(hào)：820233