基于集群的實時系統(tǒng)模型檢查技術(shù)研究與實現(xiàn).pdf

1、隨著計算機技術(shù)的飛速發(fā)展，實時系統(tǒng)(real-timesystem)的應(yīng)用日益廣泛。在實際應(yīng)用中，隨著實時系統(tǒng)規(guī)模不斷擴大、功能不斷增強，嵌入其中的軟件復(fù)雜程度也在迅速增加，從而導(dǎo)致實時系統(tǒng)運行時軟件出現(xiàn)錯誤的可能性也在增加。實時系統(tǒng)軟件運行過程中出現(xiàn)的任何一點差錯將會導(dǎo)致巨額經(jīng)濟損失、時間浪費，甚至人員傷亡。為保證實時系統(tǒng)軟件的正確性和安全性，提高其運行的可靠性，人們采取了許多的技術(shù)手段，其中形式化方法(formalmethods)起

2、到了重要的作用。 一般來說，形式化驗證(formalverification)技術(shù)包括關(guān)于規(guī)格說明性質(zhì)的定理證明(theoremproving)技術(shù)和模型檢查(modelchecking)技術(shù)。本文主要研究實時系統(tǒng)的模型檢查技術(shù)。 模型檢查的主要思想是構(gòu)造系統(tǒng)的有限狀態(tài)模型并窮盡搜索系統(tǒng)的整個狀態(tài)空間以檢查系統(tǒng)模型是否滿足期望的性質(zhì)。它有兩種實施方案：時序邏輯模型檢查和基于自動機理論的模型檢查，它的關(guān)鍵問題是狀態(tài)組合爆炸

3、。 將基于自動機理論的模型檢查技術(shù)作時間上的擴充可以驗證實時系統(tǒng)。狀態(tài)組合爆炸問題在實時系統(tǒng)模型檢查中表現(xiàn)得更為突出。它不但來源于進程組合(processcomposition)和數(shù)據(jù)域(datadomain)，還來源于時間域(timedomain)。傳統(tǒng)的優(yōu)化技術(shù)只是從一定程度上緩解了狀態(tài)爆炸，并不能從根本上解決問題，因為單機的內(nèi)存和CPU的能力是有限的。 近年來，高性能計算技術(shù)飛速發(fā)展，為在一個小的實驗室組建“個人超

4、級計算機”提供了可能。本文提出了一種基于集群的實時系統(tǒng)模型檢查技術(shù)，希望為從根本上解決狀態(tài)組合爆炸問題提供一種新的途徑。 我們選擇時間自動機(TimedAutomata)描述實時系統(tǒng)的行為和性質(zhì)，通過可達性分析算法驗證系統(tǒng)模型是否滿足期望的性質(zhì)，用C++開發(fā)了一個串行實時系統(tǒng)模型檢查器-RAModelChecker(ReachabilityAnalysisModelChecker)。 然后，我們結(jié)合高性能計算并行編程技術(shù)

5、，引入動態(tài)負載平衡和On-the-fly技術(shù)，對RAModelChecker進行并行化處理，用C++和MPI(MessagePassingInterface)設(shè)計并實現(xiàn)了一個并行實時系統(tǒng)模型檢查器—PRAModelChecker(ParallelReachabilityAnalysisModelChecker)。 最后，我們選擇兩個典型的實例對PRAModelChecker的性能進行分析。實驗表明，將實時系統(tǒng)模型檢查技術(shù)并行化是