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

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

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

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

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

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