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

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

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

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