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

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

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

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