問題框架理論中領(lǐng)域因果行為形式化驗(yàn)證的研究.pdf

1、近年來，隨著計(jì)算機(jī)產(chǎn)業(yè)的快速發(fā)展，軟件和信息技術(shù)服務(wù)業(yè)規(guī)模不斷擴(kuò)大，復(fù)雜程度不斷提高，一部分軟件產(chǎn)品在研發(fā)過程中由于經(jīng)費(fèi)，人力等原因造成工程進(jìn)度滯后，軟件質(zhì)量無法滿足設(shè)計(jì)要求，逐漸脫離前期需求標(biāo)準(zhǔn)。從軟件工程的角度看，決定軟件項(xiàng)目成敗與否的主要原因是需求，需求分析工作的好壞對(duì)最終軟件產(chǎn)品的質(zhì)量具有重要意義。尤其在安全攸關(guān)(Safety-Critical)的重大科研項(xiàng)目當(dāng)中，前期的需求分析直接影響項(xiàng)目的研發(fā)進(jìn)度和開發(fā)質(zhì)量，需求失敗或是需求

2、工作的不完整不僅會(huì)延緩工程進(jìn)度，更可能會(huì)對(duì)整個(gè)項(xiàng)目造成不可預(yù)估的損失。因此在實(shí)際項(xiàng)目開發(fā)過程中，我們應(yīng)該正視需求分析對(duì)整個(gè)系統(tǒng)的作用，保證需求分析工作的完整性。
　　作為一種需求分析方法，問題框架理論強(qiáng)調(diào)現(xiàn)實(shí)世界對(duì)軟件系統(tǒng)的作用，通過構(gòu)建上下文圖、問題圖，運(yùn)用領(lǐng)域間的問題漸變等方法將用戶需求推演變換，實(shí)現(xiàn)用戶需求到軟件規(guī)約的平滑變換。然而，目前基于問題框架方法的建模及問題漸變的實(shí)現(xiàn)主要依賴于需求分析員的直覺和經(jīng)驗(yàn)，這在一定程度上限

3、制了需求分析的嚴(yán)謹(jǐn)性和可跟蹤性，特別是在分析安全攸關(guān)軟件系統(tǒng)的需求時(shí)，問題模型中起關(guān)鍵作用的領(lǐng)域如果出現(xiàn)期望的狀態(tài)不可達(dá)或非良構(gòu)等問題，所導(dǎo)出的軟件規(guī)約的正確性無法保證，缺少形式化證據(jù)的支持和論證。因此，問題模型中領(lǐng)域間遷移關(guān)系的形式化驗(yàn)證對(duì)業(yè)務(wù)系統(tǒng)特別是安全攸關(guān)系統(tǒng)的軟件規(guī)約的獲取和處理具有重要的理論意義和實(shí)際應(yīng)用價(jià)值。模型檢驗(yàn)技術(shù)作為一種形式化驗(yàn)證方法與其它驗(yàn)證技術(shù)或者方法相比有很多優(yōu)點(diǎn)，最重要的就是其高度自動(dòng)化，可對(duì)有限狀態(tài)結(jié)構(gòu)空

4、間進(jìn)行自動(dòng)化的系統(tǒng)校驗(yàn)，并對(duì)系統(tǒng)規(guī)約描述進(jìn)行改進(jìn)。作為模型檢驗(yàn)的一個(gè)分支，符號(hào)模型檢驗(yàn)方法不但繼承了模型檢驗(yàn)高度自動(dòng)化的特點(diǎn)，同時(shí)一定程度上避免了狀態(tài)爆炸問題，處理問題的規(guī)模也可以隨之增大。該驗(yàn)證方法用一系列的布爾表達(dá)式來表示系統(tǒng)所滿足的所有狀態(tài)及狀態(tài)間的遷移關(guān)系，布爾表達(dá)式則以壓縮的方式存儲(chǔ)在有序二叉判定圖OBDD(Ordered Binary Decision Diagram)中。
　　本文基于問題框架和符號(hào)模型驗(yàn)證理論，提出

5、一套對(duì)關(guān)鍵問題領(lǐng)域模型內(nèi)狀態(tài)遷移關(guān)系的驗(yàn)證方法，隱式映射出了外部共享現(xiàn)象和內(nèi)部狀態(tài)變化事件的對(duì)應(yīng)規(guī)則，從而確定該領(lǐng)域外部共享現(xiàn)象之間具有的因果關(guān)系，為問題漸變的實(shí)現(xiàn)提供可靠的保障。同時(shí)，論文將問題框架理論和符號(hào)模型驗(yàn)證方法相結(jié)合，通過模型校驗(yàn)確定因果關(guān)系進(jìn)而為問題漸變提供變換的形式化依據(jù);定義了Kripke結(jié)構(gòu)和UML狀態(tài)機(jī)子集一對(duì)一的映射規(guī)則，將UML狀態(tài)機(jī)轉(zhuǎn)換為形式化驗(yàn)證工具的輸入語言，通過驗(yàn)證可達(dá)性性質(zhì)確定遷移路徑，篩選出具有因果