SPIN模型檢測的研究與應(yīng)用.pdf

1、軟件是否可信賴己成為一個國家的經(jīng)濟、國防等系統(tǒng)能否正常運轉(zhuǎn)的關(guān)鍵因素之，尤其在一些諸如核反應(yīng)堆控制、航空航天以及鐵路調(diào)度等安全悠關(guān)(safety-critical)領(lǐng)域更是如此。這類系統(tǒng)要求絕對安全可靠，不容半點疏漏，否則將導(dǎo)致災(zāi)難性后果。如1861年8月英國克萊頓隧道事故，就是由于協(xié)議的不完整性造成的，還有1996年6月4日，歐洲航天局阿麗亞娜(Ari-ane)501火箭因為其控制軟件的規(guī)范和設(shè)計錯誤而導(dǎo)致發(fā)射37秒后爆炸。類似的報道

2、屢見不鮮，如何確保這些系統(tǒng)的可靠性成為計算機科學(xué)與控制論領(lǐng)域共同關(guān)注的一個焦點問題。 據(jù)統(tǒng)計，在美國每年要花去3000億美金用來雇傭程序員專門來解決程序的BUG，而這個工作就占據(jù)了整個產(chǎn)品開發(fā)周期40％～60％的時間。盡管花費了這么大量的人力和物力來排除BUG，他們還是不能保證軟件沒有錯誤。 為了從根本上保證軟件系統(tǒng)的可靠安全，包括圖靈獎得主A.PnDeli在內(nèi)的許多計算機科學(xué)家都認為，采用形式化方法(formalmet

3、hds)對系統(tǒng)進行形式化驗證和分析，是構(gòu)造可靠安全軟件的一個重要途徑。模型檢測技術(shù)是形式驗證方法中的一種。而獲得ACM(AssociationforComputingMachinery)軟件系統(tǒng)獎(SoftwareSystemsAward)的SPIN就是著名的模型檢測工具之一。 典型的SPIN工作模式是首先對并發(fā)式系統(tǒng)或分布式算法的規(guī)范建立高標準的模型，在確認沒有語法錯誤后，對系統(tǒng)的交互進行模擬，直到確認系統(tǒng)設(shè)計擁有預(yù)期的行為，

4、然后SPIN產(chǎn)生一個用C語言描述的驗證程序，經(jīng)檢驗機編譯后被執(zhí)行，執(zhí)行中如果發(fā)現(xiàn)了違背正確性說明的任何反例，則反饋給交互模擬機，通過重現(xiàn)細節(jié)剔除引起錯誤的原因。 本文首先詳細介紹了著名的模型檢測工具SPIN的歷史、發(fā)展與特點，討論了使用SPIN對網(wǎng)絡(luò)通信協(xié)議分析的方法。本文所做的主要工作、技術(shù)難點與創(chuàng)新處如下： ●SPIN(SimplePromelaInterpreter)是適合于并行系統(tǒng)，尤其是協(xié)議一致性的輔助分析驗證

5、工具，本文討論了在Win32下和Cygwin/Linux/Unix下對SPIN的安裝和使用。 ●使用SPIN的最簡單的方式是使用圖形界面XSPIN，圖形界面獨立于SPIN運行，輔助產(chǎn)生和選擇相應(yīng)的SPIN命令，XSPIN在后臺運行SPIN得到期望的輸出值，XSPIN知道什么時候怎么樣去編譯模型檢測的代碼，也知道什么時候如何去執(zhí)行它，所以可以不用記住所有的參數(shù)。本文介紹了在Cygwin下安裝和使用SPIN的圖形界面工具XSPIN。

6、 ●Promela(Protocol/ProcessMetaLanguage)是用來對有限狀態(tài)系統(tǒng)進行建模的形式描述語言，本文闡述了如何使用Promela語言對協(xié)議進行描述。 ●AB協(xié)議是最早的端到端的通信協(xié)議之一，用SPIN對AB協(xié)議進行分析從而得到協(xié)議中不容易發(fā)現(xiàn)的錯誤。 ●使用SPIN的圖形界面XSPIN對上述協(xié)議進行分析得到直觀的進程之間信息的交互圖。 ●SPIN不僅可以用來驗證協(xié)議的正確性，也可