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

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

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

• 摘要5-6
• Abstract6-9
• 第1章 緒論9-12
• 1.1 研究背景9-10
• 1.2 研究內(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é)議的分析方法簡介14
• 2.2 形式化方法概述14-15
• 2.3 形式化分析方法分類15-19
• 2.3.1 信任邏輯方法15-16
• 2.3.2 定理證明方法16
• 2.3.3 模型檢測方法16-19
• 2.3.4 其他通用形式方法19
• 2.4 模型檢測技術(shù)19-20
• 2.4.1 模型檢測方法現(xiàn)狀19-20
• 2.4.2 模型檢測與其他形式化方法的比較20
• 2.5 常見的模型檢測工具20-22
• 2.6 本章小結(jié)22-23
• 第3章 協(xié)議的模型檢測工具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模型檢驗理論基礎(chǔ)24-28
• 3.2.1 線性時序邏輯LTL24-26
• 3.2.2 有限自動機26-27
• 3.2.3 SPIN基本算法27-28
• 3.3 建模語言PROMELA28-31
• 3.4 本章小結(jié)31-32
• 第4章 基于SPIN的電費代繳協(xié)議的模型檢測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 電費代繳協(xié)議的說明36-39
• 4.2 電費代繳協(xié)議的形式化描述39-45
• 4.2.1 協(xié)議的PROMELA模型結(jié)構(gòu)39-41
• 4.2.2 協(xié)議的主體狀態(tài)與行為描述41-45
• 4.3 協(xié)議驗證的屬性描述45-46
• 4.4 協(xié)議行為的模擬分析46-50
• 4.5 協(xié)議屬性驗證結(jié)果分析50-52
• 4.6 本章小結(jié)52-53
• 第5章 支付寶定單代付協(xié)議與手機充值協(xié)議的模型檢測53-67
• 5.1 支付寶定單代付協(xié)議53-59
• 5.1.1 協(xié)議內(nèi)容與說明53-54
• 5.1.2 協(xié)議的形式化描述54-58
• 5.1.3 協(xié)議屬性的提取與描述58-59
• 5.2 支付寶定單代付協(xié)議模擬與檢測59-61
• 5.2.1 基于SPIN的協(xié)議行為模擬59-60
• 5.2.2 協(xié)議屬性的驗證60-61
• 5.3 手機充值協(xié)議61-64
• 5.3.1 手機充值協(xié)議描述61-62
• 5.3.2 協(xié)議的PROMELA語言描述62-64
• 5.4 協(xié)議的SPIN模擬分析與檢測64-66
• 5.5 本章小結(jié)66-67
• 第6章 總結(jié)與展望67-69
• 6.1 論文總結(jié)67
• 6.2 展望67-69
• 參考文獻69-72
• 致謝72

【參考文獻】

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

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

2 錢俊彥;趙嶺忠;;基于自動機理論的符號模型檢驗[J];蘭州理工大學(xué)學(xué)報;2008年05期

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

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

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

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

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

8 支小莉,陸鑫達,戎璐;Promela行為模型的自動抽象[J];計算機工程;2004年16期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：820233