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

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

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

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

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

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

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