LINUX內(nèi)核進(jìn)程間通信的模型檢測(cè)研究.pdf

1、LINUX操作系統(tǒng)繼承了UNIX的基本設(shè)計(jì)思想，是當(dāng)今為人們所公認(rèn)的具有較強(qiáng)的安全性和穩(wěn)定性的系統(tǒng)。對(duì)于這樣一種多任務(wù)、多用戶的操作系統(tǒng)來說，怎樣進(jìn)行進(jìn)程間通信(InterProcess Communication，IPC)，是個(gè)不可忽視的重大問題。對(duì)進(jìn)程間通信的正確性的驗(yàn)證，成為一個(gè)值得共同關(guān)注的有著相當(dāng)意義的研究課題。模型檢測(cè)現(xiàn)已成為驗(yàn)證系統(tǒng)的趨勢(shì)，本文正是采用了這種方法對(duì)LINUX進(jìn)程間通信進(jìn)行驗(yàn)證。 管道進(jìn)程間通信作為最

2、早的通信方式之一，通信機(jī)制相對(duì)而言較為簡(jiǎn)單。本文首先對(duì)LINUX內(nèi)核2.6.0版本中管道通信的相關(guān)源代碼進(jìn)行分析，抽取出用有限狀態(tài)自動(dòng)機(jī)(Finite State Automaton，F(xiàn)SA)描述的形式化模型，繼而向Promela代碼轉(zhuǎn)換。隨后采用線性時(shí)序邏輯(Linear-time Temporal Logic，LTL)公式表達(dá)期望系統(tǒng)滿足的屬性，通過Xspin工具進(jìn)行模型檢測(cè)，驗(yàn)證了系統(tǒng)的有界性和可終止性，并就實(shí)際進(jìn)程間通信中容易發(fā)

3、生的問題提出了改進(jìn)方案。 Socket進(jìn)程間通信是本文的第二個(gè)研究重點(diǎn)，從概念上說，與管道通信比較相似，但實(shí)現(xiàn)上相距甚遠(yuǎn)，也更為復(fù)雜，是能夠應(yīng)用于非近親進(jìn)程之間的通信方式。研究了LINUX內(nèi)核中與socket相關(guān)的源代碼，抽取服務(wù)器端和客戶端的形式化模型。將形式化模型轉(zhuǎn)換成Promela代碼之前，添加了一個(gè)中間步驟：為每個(gè)進(jìn)程的每個(gè)狀態(tài)建立狀態(tài)轉(zhuǎn)換表，縮小形式化模型與Promela代碼的差距。在向Promela代碼轉(zhuǎn)換的過程中