模型檢測技術(shù)在農(nóng)業(yè)生產(chǎn)中的應(yīng)用

模型檢測技術(shù)在農(nóng)業(yè)生產(chǎn)中的應(yīng)用

1限狀態(tài)系統(tǒng)的技術(shù)linux操作系統(tǒng)的出現(xiàn)是計算機科學(xué)發(fā)展史的重要里程碑。它誕生于1969年的貝爾實驗室。1991年,LinusTorvalds等人基本上按照UNIX的設(shè)計,開發(fā)出一個真正可以使用的UNIX內(nèi)核,并稱之為LINUX。可以說LINUX內(nèi)核是目前覆蓋面最廣的一體化內(nèi)核,它的安全性和穩(wěn)定性也眾所周知。作為多用戶、多任務(wù)的操作系統(tǒng),進程間通信的重要性不可小覷,因此對其進行模型檢測成為一個意義重大的研究課題。模型檢測是一種強大的自動分析驗證有限狀態(tài)系統(tǒng)的技術(shù),它將所需驗證的系統(tǒng)及屬性作為模型檢測工具的輸入,以判斷屬性的正確性,是有限狀態(tài)驗證(FiniteStateVerification)的方法之一,另外還有兩種分別是流方程(FlowEquations)和數(shù)據(jù)流分析(DataFlowAnalysis)。迄今為止已開發(fā)出多種分析驗證工具,如模型檢測的SMV(SymbolicModelChecking),SPIN(SimplePromelaINterpreter),流方程的INCA(IntegerNecessaryConditions)以及數(shù)據(jù)流分析的FLAVERS(FLowAnalysisforVERificationofSystems)。美國的NASA實驗室還專門開發(fā)了一種針對JAVA的工具——JPF(JavaPathFinder),對JAVA程序進行模型檢測。本文采用的是SPIN工具。它是一種由美國貝爾實驗室開發(fā)的模型檢測工具,應(yīng)用了偏序規(guī)約、onthefly等技術(shù),大大提高了模型檢測的效率,減小了狀態(tài)空間,可以用斷言(assertion)或線性時態(tài)邏輯(LTL)來驗證系統(tǒng)屬性,已經(jīng)成功地應(yīng)用于協(xié)議驗證、分布式系統(tǒng)驗證和軟件驗證中。本文分析了LINUX2.4.0版本的基于管道的進程間通信的內(nèi)核源碼,從中提取形式化模型,再用SPIN進行模型檢測。文章結(jié)構(gòu)如下:第2節(jié)簡單介紹模型檢測分析工具SPIN;第3節(jié)是LINUX進程間通信的代碼分析和形式化建模;第4節(jié)對它進行模型檢測,并得出實驗結(jié)果;最后總結(jié)全文。2spin模型探測器2.1promela描述SPIN(SimplePromelaINterpreter)是適合于并發(fā)系統(tǒng)的一種模型檢測分析驗證工具。它以PROMELA作為輸入語言,對于給定的一個使用PROMELA描述的系統(tǒng)模型,SPIN可以對其執(zhí)行進行隨意的模擬,也可以生成一個C代碼程序,然后對系統(tǒng)的正確性進行有效的檢驗。PROMELA(PROcessMEtaLAnguage)是用來對有限狀態(tài)系統(tǒng)進行建模的形式描述語言。它類似于C程序語言,允許動態(tài)創(chuàng)建并行的進程,并可以在進程之間通過消息通道進行同步或異步通信。一個PROMELA模型由進程、消息通道、變量和全局對象組成,相當(dāng)于一個有限轉(zhuǎn)換系統(tǒng)。其大體結(jié)構(gòu)為:類型說明、通道說明、變量說明、進程說明、初始進程。如圖1所示,SPIN首先從一個PROMELA描述的抽象模型開始,經(jīng)過分析,沒有語法錯誤后,對系統(tǒng)的交互進行模擬,直到確認(rèn)系統(tǒng)設(shè)計擁有預(yù)期的行為;然后,SPIN將產(chǎn)生一個用C語言描述的驗證程序,經(jīng)驗證機編譯后被執(zhí)行。執(zhí)行中如果發(fā)現(xiàn)了違背正確性說明的任何反例,則可反饋給交互模擬機,通過重現(xiàn)細(xì)節(jié)找出引發(fā)錯誤的原因。2.2線性態(tài)邏輯的生成規(guī)則SPIN的工作原理基于這樣一個事實,即分布式系統(tǒng)中異步進程的行為能夠用有限狀態(tài)自動機(FSA)來模擬。定義1(有限狀態(tài)自動機,FSA)有限狀態(tài)自動機A是一個五元組(S,s0,L,T,F),其中:S={s0,s1,s2,…,sn}是有限狀態(tài)集合;s0是FSA的初始狀態(tài),s0∈S;L是觸發(fā)狀態(tài)遷移的事件的有限集合;T是狀態(tài)之間的遷移關(guān)系,T?(S×L×S);F是終止?fàn)顟B(tài),F?S。定義2(同步積)FSAP和B的同步積是一個FSAA=(S,s0,L,T,F),其中:A.S是P′.S×B.S的笛卡爾積,P′是P的stutter閉包;A.S0是二元組(P.s0,B.s0);A.L是P′.L×B.L的笛卡爾積;A.T是(t1,t2)對,t1∈P′.T且t2∈B.T;A.F是(s1,s2)∈A.S對的集合,s1∈P.F∨s2∈B.F。定義3(異步積)一個FSA有限集合A1,…,An的異步積是一個FSAA=(S,s0,L,T,F),其中:A.S是A1.S×…×An.S笛卡爾積;A.s0是n元組(A1.s0,…,An.s0);A.L是A1.L∪…∪An.L;A.T是元組集合((x1,…,xn),I,(y1,…,yn)),其中?i,1≦i≦n,(xi,I,yi)∈Ai.T,且?j,1≦j≦n,j≠i→(xj≡yj);A.F是A.S的子集,滿足?(A1.s,…,An.s)∈A.F,其中?i,Ai.s∈Ai.F。定義4(線性時態(tài)邏輯,LTL)線性時態(tài)邏輯常用于描述需驗證的屬性,它由原子命題、邏輯連接符和模態(tài)算子組成。邏輯連接符包括?(非)、∨(或)、∧(與)。模態(tài)算子包括〈〉(Eventually)、(Always)。設(shè)p為原子命題,LTL公式的產(chǎn)生規(guī)則如下:φ∷=p|(?φ)|(φ∧φ)|(φ∧φ)|(φ)|(〈〉φ)其中〈〉表示現(xiàn)在或以后某一狀態(tài),表示現(xiàn)在和以后所有狀態(tài)。例如,〈〉p表示p無限多次為真,〈〉p表示從某個時刻起,p一直為真。定義5(全局系統(tǒng)自動機S)S=B?∏i=1nAiS=B?∏i=1nAi其中,B表示Büchi自動機,由給定的LTL表達(dá)式轉(zhuǎn)換而成;Ai表示由進程形式化得到的自動機;?表示兩個自動機的同步積;∏表示若干自動機的異步積。假設(shè)系統(tǒng)A有n個進程,形式化成n個自動機:A1,A2,…,An,考慮一個LTL表達(dá)式f以及相應(yīng)的?f形成的Büchi自動機B,應(yīng)用自動機驗證理論,便能通過計算全局系統(tǒng)自動機S來檢測系統(tǒng)A是否滿足屬性f。3linux進程之間的通信建模3.1進程通過管道進行通信對于LINUX這種多任務(wù)、多用戶的操作系統(tǒng)來說,進程間通信是一種非常重要甚至必不可少的基本手段和設(shè)施。本文針對的是通過管道(Pipe)進行的進程間通信。父進程與子進程之間,或者兩個兄弟進程之間,可以通過系統(tǒng)調(diào)用建立起一個單向的通信管道,這種管道只能由父進程建立。管道兩端的進程將該管道看成文件。一個進程往管道中寫入數(shù)據(jù),另一個進程從管道中讀取,即管道的寫端和讀端,它們遵循先入先出的原則,且通信是單向的。圖2展示了父子進程通過管道進行通信。如圖2所示,進程A創(chuàng)建一個管道,創(chuàng)建完成時管道的讀端和寫端都在進程A中。進程A通過fork()創(chuàng)建出進程B,在fork()的過程中進程A的打開文件表原封不動復(fù)制到進程B中。進程A關(guān)閉管道讀端,而進程B關(guān)閉管道寫端。于是,進程B就能夠從管道中讀取進程A寫入的數(shù)據(jù)。對于這樣的進程間管道通信,有可能出現(xiàn)以下幾個問題:第一,進程A有大量的數(shù)據(jù)需要寫入管道,導(dǎo)致緩沖區(qū)溢出,這是非常危險的。據(jù)統(tǒng)計,通過緩沖區(qū)溢出進行的攻擊占所有系統(tǒng)攻擊總數(shù)的80%以上。第二,進程A、進程B以及管道,三者最終是否能夠到達(dá)一個穩(wěn)定的正確狀態(tài),這是管道通信正常工作的基本保證。第三,這種情況相對復(fù)雜,當(dāng)進程A只寫入了部分?jǐn)?shù)據(jù)而管道已滿時,要待B讀走一些數(shù)據(jù)后才能繼續(xù)寫入,而B讀完之后退出,A還有未寫完的數(shù)據(jù),這時會發(fā)生什么狀況呢?在下面的章節(jié)中,將一一詳細(xì)解答。3.2管道、管道的建?；贚INUX管道通信的基本思想,本文針對相關(guān)源代碼(主體代碼在linux/fs/pipe.c中)進行形式化建模。使用有限狀態(tài)自動機(FSA)描述模型。將管道、管道讀端以及寫端看作三個實體,建立三個相應(yīng)的FSA。三個有限狀態(tài)自動機顯然會涉及三個實體的互相交互,加上并發(fā)機制本身的不確定性因素,無疑給建模工作帶來了困難。由于篇幅的限制,本文不對LINUX源碼做具體講解。3.2.1管道斷裂接口通過分析linux/fs/pipe.c源代碼,了解到管道機制的主體是系統(tǒng)調(diào)用pipe(),系統(tǒng)調(diào)用的主體是do_pipe(),以此建立管道。管道創(chuàng)建后,可通過它進行讀寫操作,實現(xiàn)進程間通信。當(dāng)讀者或?qū)懻呓Y(jié)束時,管道進入預(yù)關(guān)閉狀態(tài),直到?jīng)]有讀者和寫者,管道才正式關(guān)閉。若準(zhǔn)備寫入數(shù)據(jù)時檢測到?jīng)]有讀者,則宣布管道斷裂。根據(jù)管道的特性對其形式化建模,見圖3(a)。圓角矩形表示管道所處的狀態(tài),箭頭表示狀態(tài)的遷移,箭頭上的標(biāo)識說明遷移的觸發(fā)條件或動作。3.2.2運行管道進入接口通過對源碼的分析了解到,管道的讀端總是處于一個for循環(huán)中,通過系統(tǒng)調(diào)用read()從管道中讀取數(shù)據(jù)進行處理,處理完后接著讀取。對管道的讀操作,在內(nèi)核中經(jīng)過sys_read()和數(shù)據(jù)結(jié)構(gòu)read_pipe_fops中的函數(shù)指針而到達(dá)主體函數(shù)pipe_read()。調(diào)用該函數(shù),進行管道的讀取操作。如果此時管道緩沖區(qū)中已有數(shù)據(jù),則開始讀取;然而,如果管道中沒有數(shù)據(jù),一般就需要進入等待狀態(tài)。其中,又有兩種情況例外:·此時寫者計數(shù)器已經(jīng)為0,即沒有寫者,說明管道中不會再被寫入數(shù)據(jù)。在這種情況下等待沒有意義?！す艿绖?chuàng)建時,設(shè)置了標(biāo)志位NOBLOCK,表示當(dāng)讀者讀取不到管道中的數(shù)據(jù)時,不被阻塞。此時也無需等待。讀者在等待的過程中,如果寫端向管道中寫入了數(shù)據(jù),則它重新進入讀取狀態(tài)。當(dāng)讀者完成了讀取操作,就自然進入到最終的完成狀態(tài)。同樣地,對于管道讀端建立的模型如圖3(b)。3.2.3管道文化檢查管道寫端的操作與讀端類似,只是當(dāng)寫端請求寫入的長度小于管道緩沖區(qū)容量時,內(nèi)核需要保證寫入操作的原子性。也就是說,在管道空閑區(qū)域足夠大,能容納寫入的全部數(shù)據(jù)時才開始進行一次性寫入操作。然而,當(dāng)請求寫入的長度大于管道緩沖區(qū)時,就不保證寫入的原子性,一旦有空閑區(qū)域就寫入,未寫完的數(shù)據(jù)待讀端讀取部分?jǐn)?shù)據(jù)后繼續(xù)寫入。最終同樣進入完成狀態(tài)。建立的模型如圖3(c)所示。3.3管道斷裂的檢測程序構(gòu)造形式化建模后,將它轉(zhuǎn)化成PROMELA。以管道模型部分代碼為例:proctypePipe(){do∷Pipe_State==WRITTEN→atomic{if∷write==1→skip;if∷(writers>0&&readers==0→Pipe_State=BROKEN;read=0;write=0∷else→skipif∷(write==0&&Writer_State!=WAIT)→Pipe_State=ReadyCLOSEif}∷……od}進程通過do和od循環(huán)判斷管道所處的狀態(tài),atomic{}中的內(nèi)容表示不被打斷的原子操作。如果管道當(dāng)前的狀態(tài)為WRITTEN,表示管道的寫端正在向管道中寫入數(shù)據(jù)。此時,如果檢測到管道另一端沒有讀者,則寫操作無意義。于是,內(nèi)核發(fā)出SIGPIPE信號,隨即管道斷裂。管道寫端完成寫操作后,管道狀態(tài)則遷移到ReadyCLOSE(預(yù)關(guān)閉)。4模型檢測系統(tǒng)實驗環(huán)境:CPU3.06GHz,內(nèi)存512M,硬盤80G,操作系統(tǒng)WinXP,模型檢測器SPIN4.3.0。通過SPIN對系統(tǒng)進行模擬,結(jié)果顯示,在設(shè)置了不同參數(shù)的條件下,它能很好地模擬出系統(tǒng)各條不同的執(zhí)行路徑,并且最終到達(dá)正確的結(jié)束狀態(tài)。4.1驗證是檢驗系統(tǒng)的邊界不能超過其邊界的情況;正如3.1節(jié)中所述,進程間管道通信存在幾個重要的問題,換言之,它具有幾個關(guān)鍵屬性。因此,本文通過模型檢測的方法對其屬性正確性進行驗證是非常有意義的。屬性常用線性時態(tài)邏輯(LTL)表達(dá)式描述,并作為SPIN的輸入。首先,驗證有界性,即變量不能超過它的邊界。例如,寫端向管道中寫入數(shù)據(jù)后,管道長度為pipe_len,該長度不允許超過管道緩沖區(qū)的總長bufMax,否則會導(dǎo)致緩沖區(qū)溢出,從而發(fā)生不可預(yù)測的危險。用LTL公式來表示:(pipe_len<=bufMax)。如果出現(xiàn)越界的情況,則不滿足該屬性。作為對比,這里將檢驗的性質(zhì)改為(pipe_len<bufMax),以斷言的形式插入程序中,重新檢驗一次。其次,驗證可終止性,也就是檢驗系統(tǒng)最終是否都達(dá)到有效的結(jié)束狀態(tài),以保證進程間通信的正常工作。具體的終止?fàn)顟B(tài)在系統(tǒng)驗證的結(jié)果中列出(見表1),此處不一一贅述。4.2實驗過程及改進本文使用Xspin對系統(tǒng)進行模型檢測,這是一個獨立運行于SPIN的圖形界面軟件,圖4顯示其工作界面。對于LTL的第一個公式,在Xspin中表示如圖4(a),驗證結(jié)果顯示該性質(zhì)有效。插入斷言后,再次檢驗的結(jié)果說明系統(tǒng)不滿足性質(zhì),詳細(xì)輸出見圖4(b)?？梢钥吹?詳細(xì)輸出結(jié)果說明系統(tǒng)在第78層違反了屬性,并且生成了trail文件(即SPIN生成的反例),以便查找錯誤原因。隨后列出SPIN的版本信息、對整個狀態(tài)空間進行搜索之后獲得的信息(包括聲稱、斷言、循環(huán)檢查和無效最終狀態(tài))、狀態(tài)矢量、可達(dá)深度和錯誤數(shù)的信息(包括存儲狀態(tài)、匹配狀態(tài)、遷移和原子操作數(shù))、哈希沖突以及實驗所使用的內(nèi)存信息。從圖1中得知,生成的反例可以反饋回模擬器再次進行系統(tǒng)模擬,此時發(fā)現(xiàn)SPIN結(jié)束在斷言之后:spin:line276“pan_in”,Error:assertionviolated(見圖4(c)),其中pan_in是模型經(jīng)編譯后生成的C程序。以此模擬輸出為基礎(chǔ),能夠迅速找到錯誤并加以解決。通過設(shè)置不同的參數(shù),Xspin仿真輸出的結(jié)果顯示管道、管道寫端以及管道讀端的最終停止?fàn)顟B(tài)(見表1)。第一列是各實體名稱。第二列說明管道到達(dá)關(guān)閉狀態(tài),寫端和讀端都到達(dá)完成狀態(tài)。這是管道完成通信的最佳狀態(tài)。第三列顯示此時寫端還能夠進行寫操作,但是讀端已經(jīng)讀取完畢,并且沒有讀者再讀管道,因此管道斷裂。這也是正確結(jié)束的狀態(tài)。第四列說明此時寫端未寫完數(shù)據(jù),由于管道已滿而進入等待,讀端讀取完后結(jié)束,于是管道斷裂。從實驗結(jié)果可以看出,系統(tǒng)滿足可終止性。然而,第三種情況(第四列)常常導(dǎo)致不完整的通信,即3.1節(jié)中