復(fù)雜信息系統(tǒng)模型的形式化驗證方法研究.pdf

1、軟件的質(zhì)量和可靠性問題由來己久。目前，雖然軟件分析、設(shè)計和測試技術(shù)仍是保障軟件可靠性的主要手段，但是由于人們對軟件系統(tǒng)分布式處理，并發(fā)處理，實時處理等能力要求的日益增強，使軟件系統(tǒng)正日益趨向高度的復(fù)雜化，導(dǎo)致上述方法仍然不能完全滿足開發(fā)高可靠軟件系統(tǒng)的需要。模型檢測作為一種形式化驗證技術(shù)因其嚴(yán)格的數(shù)學(xué)基礎(chǔ)、全自動的驗證過程，以及早期在硬件系統(tǒng)和協(xié)議驗證中的成功應(yīng)用而倍受學(xué)術(shù)界和產(chǎn)業(yè)界的關(guān)注。但是在軟件工程各階段中結(jié)合模型檢測，全面、自動

2、的分析和驗證復(fù)雜信息系統(tǒng)的需求、設(shè)計及性能模型、提高軟件的安全性和可靠性尚處于探索階段。針對上述問題，論文在軟件工程中結(jié)合形式化方法與模型檢測技術(shù)，分別從需求分析層面、模型設(shè)計層面以及性能設(shè)計層面研究具有分布式、并發(fā)和實時行為特性的復(fù)雜信息系統(tǒng)形式化建模及驗證技術(shù)：
　　 首先，對形式化方法及模型檢測技術(shù)的相關(guān)研究進(jìn)行了綜述，闡述了復(fù)雜信息系統(tǒng)的行為特征，分析了復(fù)雜信息系統(tǒng)形式化建模及驗證工作的重點與難點，總結(jié)了該領(lǐng)域存在的問題

3、以及未來的研究方向。
　　 其次，為驗證復(fù)雜信息系統(tǒng)需求模型設(shè)計的正確性，將復(fù)雜信息系統(tǒng)的軟件需求劃分為頂層需求和技術(shù)層面需求，使用面向行為的抽象方法將領(lǐng)域政策建模為系統(tǒng)的頂層需求模型，并用RSL對其進(jìn)行形式化規(guī)約。為驗證及細(xì)化頂層需求模型，本文通過定義RSL語法及語義的轉(zhuǎn)換規(guī)則將頂層需求模型的RSL規(guī)約轉(zhuǎn)換為Promela模型，將頂層需求的性質(zhì)規(guī)約描述為時態(tài)邏輯公式，最后使用模型檢測器SPIN自動驗證頂層需求模型對性質(zhì)規(guī)約的可

4、滿足性。
　　 再次，為驗證復(fù)雜信息系統(tǒng)技術(shù)層面需求模型設(shè)計的正確性，首先用UML順序圖建模復(fù)雜信息系統(tǒng)的動態(tài)交互場景；針對UML順序圖模型缺乏精確的動態(tài)語義以及不能自動驗證模型動態(tài)性質(zhì)的問題，為UML順序圖定義遷移系統(tǒng)操作語義及其到Promela模型的轉(zhuǎn)換規(guī)則，將順序圖模型的XMI描述文件的解析信息自動轉(zhuǎn)換為Promela程序；最后，將建模系統(tǒng)需求的Promela程序和描述系統(tǒng)性質(zhì)規(guī)約的線性時序邏輯公式作為模型檢測器SPIN的

5、輸入，自動驗證系統(tǒng)技術(shù)層面需求模型設(shè)計的正確性。
　　 第四，為驗證復(fù)雜信息系統(tǒng)設(shè)計模型的正確性，以UML狀態(tài)圖為系統(tǒng)建模的主要工具，使用元組定義UML狀態(tài)圖的主要元素，從而給出一種狀態(tài)圖模型的中間表示形式將層次狀態(tài)圖轉(zhuǎn)化為平面狀態(tài)圖；基于該中間表示形式定義狀態(tài)圖模型的操作語義，設(shè)計復(fù)雜信息系統(tǒng)設(shè)計模型到NuSMV輸入模型的語義轉(zhuǎn)換規(guī)則；基于轉(zhuǎn)換規(guī)則以及設(shè)計模型的XMI文檔解析信息實現(xiàn)設(shè)計模型到NuSMV輸入模型的自動轉(zhuǎn)換過程，

6、并通過證明狀態(tài)圖的操作語義與轉(zhuǎn)換得到的NuSMV輸入模塊的操作語義為互模擬等價關(guān)系證明轉(zhuǎn)換過程的正確性；最后使用模型檢測器NuSMV驗證復(fù)雜信息系統(tǒng)設(shè)計模型對其性質(zhì)規(guī)范的可滿足性。
　　 最后，研究復(fù)雜信息系統(tǒng)實時性能設(shè)計的形式化驗證技術(shù)，在需求分析過程中使用UML協(xié)作圖建模系統(tǒng)的任務(wù)體系結(jié)構(gòu)，描述當(dāng)外部事件到達(dá)時系統(tǒng)內(nèi)部事件和任務(wù)的激活順序；用事件順序分析方法為并發(fā)任務(wù)分配執(zhí)行時間預(yù)算，將UML協(xié)作圖擴展為實時協(xié)作圖；基于實時