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

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

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

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

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

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

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