基于SCXML的WEB應(yīng)用服務(wù)的模型檢查的研究和應(yīng)用.pdf

1、隨著網(wǎng)絡(luò)及其技術(shù)的迅速發(fā)展，WEB應(yīng)用被廣泛應(yīng)用于國計民生的各個領(lǐng)域。與此同時，隨著需求量與應(yīng)用領(lǐng)域的不斷擴大，對WEB應(yīng)用的正確性、有效性和安全性等方面都提出了越來越高的要求。為最大限度減少WEB應(yīng)用的缺陷，保證和提高WEB應(yīng)用的質(zhì)量，如何對WEB應(yīng)用進行有效的驗證、測試逐漸成為人們研究所面臨的主要問題。
　　 模型檢查是對有窮狀態(tài)系統(tǒng)的一種形式化驗證方法，它基于狀態(tài)搜索的基本思想。WEB應(yīng)用的復雜性、動態(tài)性、異構(gòu)性、組成成分

2、和鏈接的多樣性等使得直接對WEB應(yīng)用進行驗證相當困難。對基于建模語言State Chart XML( SCXML)的WEB應(yīng)用進行模型檢查的研究和應(yīng)用是本文討論的重點。為避免WEB應(yīng)用模型檢查中內(nèi)存不足和狀態(tài)爆炸等問題，本文把“On-the-Fly”技術(shù)引入到針對WEB應(yīng)用的模型檢查中。本文的主要工作有：
　　 1．研究了WEB應(yīng)用建模語言SCXML。根據(jù)WEB應(yīng)用的特征，用SCXML對抽象出來的WEB應(yīng)用的關(guān)鍵的行為、性質(zhì)進行

3、表示。
　　 2．在深入分析SCXML的語法和語義的基礎(chǔ)上，在此語言的子集上，研究并提出了一個由SCXML向Büchi自動機轉(zhuǎn)換的算法，同時引用并實現(xiàn)了一個有效的算法用于從LTL公式向Büchi自動機的轉(zhuǎn)換。
　　 3．基于模型檢查的特性，針對WEB應(yīng)用的正確、安全和有效性等性質(zhì)進行驗證，采用模型檢查的“On-the-Fly”算法，實現(xiàn)了“On-the-Fly”的模型檢查系統(tǒng)，從而實現(xiàn)對WEB應(yīng)用進行有效的驗證，并用C＃