模型檢測技術在農業生產中的應用

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