速昱行 ，王金波

（1.中國(guó)科學(xué)院大學(xué)北京100190；2.中國(guó)科學(xué)院空間應(yīng)用工程與技術(shù)中心北京100094）

為了適應(yīng)航天事業(yè)的快速發(fā)展，完成繁雜的空間任務(wù)，對(duì)嵌入式軟件系統(tǒng)的可靠性、穩(wěn)定性等提出了更高的要求，Linux作為一款開(kāi)源、可裁剪、可移植的操作系統(tǒng)逐漸被應(yīng)用于國(guó)內(nèi)外航天嵌入式領(lǐng)域。

對(duì)于航天任務(wù)而言，其特殊性決定了必須在研制階段就確保星載嵌入式軟件的可靠性，否則可能會(huì)造成災(zāi)難性的后果。例如，1997年火星“探路者”號(hào)在執(zhí)行任務(wù)時(shí)，遇到系統(tǒng)頻繁重啟問(wèn)題；1996年歐洲航天局發(fā)射的一架未載人的阿麗亞娜5號(hào)火箭，在發(fā)射升空40秒鐘之后發(fā)生了爆炸。因此，對(duì)操作系統(tǒng)進(jìn)行分析和驗(yàn)證是至關(guān)重要的。目前，對(duì)于操作系統(tǒng)的測(cè)試驗(yàn)證工作，尚無(wú)明確的標(biāo)準(zhǔn)和規(guī)范，主要的方法有以下幾種[1-5]：

1）通過(guò)各種系統(tǒng)調(diào)用測(cè)試內(nèi)核功能的安全性和正確性；

2）通過(guò)第三方的測(cè)試套件（工具）對(duì)內(nèi)核進(jìn)行測(cè)試；

3）各種性能測(cè)試，如實(shí)時(shí)性測(cè)試等。

針對(duì)已有測(cè)試手段只能盡可能多的找出錯(cuò)誤和缺陷，形式化驗(yàn)證通過(guò)對(duì)系統(tǒng)所有行為狀態(tài)的模擬，可以在早期便徹底的檢測(cè)系統(tǒng)是否還存在其他問(wèn)題。模型檢測(cè)作為形式化驗(yàn)證的其中一支于近年來(lái)成功地應(yīng)用在了通用操作系統(tǒng)的分析和驗(yàn)證中[4]，特別是與數(shù)字電路和通信協(xié)議有關(guān)的設(shè)計(jì)中。同時(shí)進(jìn)程間通信（IPC）對(duì)操作系統(tǒng)的重要性不言而喻，因此對(duì)其進(jìn)行模型檢測(cè)非常有意義，也成為一個(gè)研究模型檢測(cè)對(duì)操作系統(tǒng)驗(yàn)證的切入點(diǎn)。

1 模型檢測(cè)和SPIN概述

形式化驗(yàn)證是基于用形式化語(yǔ)言描述的規(guī)格（specification）之上進(jìn)行模型（model）分析和驗(yàn)證，從而發(fā)現(xiàn)系統(tǒng)中存在的不一致性、歧義性、不完整性和競(jìng)態(tài)條件的方法。其主要手段包括模型檢測(cè)和定理證明。前者的應(yīng)用范圍限定在有限狀態(tài)并發(fā)系統(tǒng)上，可以在有限的時(shí)間和空間內(nèi)完全自動(dòng)運(yùn)行和終止；后者則被用于無(wú)限狀態(tài)的推理，但只有其中一部分可以自動(dòng)進(jìn)行，但即使驗(yàn)證性質(zhì)為真，卻可能需要無(wú)限大的時(shí)間和內(nèi)存。因此模型檢測(cè)應(yīng)用場(chǎng)景更加廣泛，可以用在中等規(guī)模的計(jì)算機(jī)上運(yùn)行[4]。

模型檢測(cè)將建立的系統(tǒng)模型及性質(zhì)作為檢測(cè)工具的輸入，一般通過(guò)深度優(yōu)先遍歷的方式進(jìn)行狀態(tài)空間搜索，從而判斷屬性正確與否。目前已經(jīng)開(kāi)發(fā)出的模型檢測(cè)工具有很多[5]，如SMV、SPIN、JPF、Isabelle/HOL、MOPS等。模型檢測(cè)一般經(jīng)過(guò)以下3個(gè)步驟：

1）建模——抽象模型提取以及轉(zhuǎn)化為能被檢測(cè)工具接受的形式；

2）刻畫(huà)——聲明模型需要滿足的性質(zhì)；

3）驗(yàn)證——分析驗(yàn)證結(jié)果（錯(cuò)誤軌跡）。

本文工作主要基于SPIN，其最大特點(diǎn)是采用了偏序規(guī)約、on the fly等技術(shù)[8]，從而狀態(tài)空間的數(shù)目得以縮減，提高了檢測(cè)效率。它的建模語(yǔ)言為Promela，可以用線性時(shí)態(tài)邏輯（LTL）和斷言（assertion）來(lái)聲明系統(tǒng)屬性，支持隨機(jī)、交互式和引導(dǎo)式模擬。SPIN的每個(gè)進(jìn)程都被看作有限狀態(tài)自動(dòng)機(jī)來(lái)建模，實(shí)際并發(fā)系統(tǒng)的全局行為就通過(guò)計(jì)算這些自動(dòng)機(jī)的異步交錯(cuò)積來(lái)得到：1）對(duì)LTL公式刻畫(huà)的系統(tǒng)性質(zhì)取反，得到Büchi自動(dòng)機(jī)P；2）計(jì)算系統(tǒng)中每個(gè)進(jìn)程的轉(zhuǎn)移子系統(tǒng)的乘積，建立Büchi自動(dòng)機(jī)S，得到模型代表的系統(tǒng)的全局行為；3）計(jì)算P與S的乘積；4）檢查最后乘積得到的自動(dòng)機(jī)，若其所能接受的語(yǔ)言為空，則表示系統(tǒng)滿足所描述的性質(zhì)，反之說(shuō)明系統(tǒng)不滿足原本定義的屬性要求。具體在軟件中操作的過(guò)程如圖1直觀所示，證明時(shí)序邏輯公式φ是否在模型M中成立（即證明M|=φ）。

圖1 SPIN模型檢測(cè)過(guò)程

Promela是SPIN的建模語(yǔ)言，其中包括的抽象對(duì)象有變量、消息、通道、進(jìn)程、遷移和全局系統(tǒng)狀態(tài)。消息通道支持會(huì)面點(diǎn)（rendezvous）或緩沖的（buffered）消息傳遞方式，實(shí)現(xiàn)同步或者異步通信。

2 Linux管道的分析驗(yàn)證

2.1 管道的描述

在Linux中，處于用戶空間的進(jìn)程擁有各自的地址空間，一般無(wú)法互相訪問(wèn)。然而多數(shù)場(chǎng)景下需要進(jìn)程間進(jìn)行相互通信，以完成系統(tǒng)的某些功能，如數(shù)據(jù)傳輸、數(shù)據(jù)共享、消息通知、進(jìn)程控制等[7]。進(jìn)程通過(guò)與內(nèi)核及其它進(jìn)程之間的互相通信來(lái)協(xié)調(diào)各自的行為。管道屬于IPC中一種使用頻率較高的通信手段，有匿名管道和命名管道之分。前者只能在父子進(jìn)程或者兄弟進(jìn)程之間使用，而后者打破了這種限制，提供了文件的路徑來(lái)識(shí)別管道，從而實(shí)現(xiàn)在沒(méi)有親緣關(guān)系的進(jìn)程之間通信，本文僅討論匿名管道。管道從本質(zhì)上說(shuō)也是文件的一種，但它又和普通的文件有所區(qū)別，它是內(nèi)核中一個(gè)大小固定的緩沖區(qū)。其具體實(shí)現(xiàn)的源代碼位于＜fs/pipe.c>中，創(chuàng)建過(guò)程如圖2所示。

圖2 管道創(chuàng)建過(guò)程

1）父進(jìn)程通過(guò)調(diào)用int pipe（int fd[2]）創(chuàng)建管道，這里得到的兩個(gè)文件描述符fd[0]、fd[1]，分別指向管道的讀端和寫(xiě)端，此時(shí)讀端和寫(xiě)端皆指向父進(jìn)程；

2）父進(jìn)程通過(guò)調(diào)用fork（）創(chuàng)建子進(jìn)程，子進(jìn)程拷貝了父進(jìn)程除某些資源之外的所有內(nèi)容，包括上一步創(chuàng)建的管道，即子進(jìn)程也有兩個(gè)文件描述符指向同一管道；

3）隨后，父進(jìn)程關(guān)閉讀端，子進(jìn)程關(guān)閉寫(xiě)端，則前者向管道中寫(xiě)入數(shù)據(jù)，而后者就可以將管道中的數(shù)據(jù)讀出，這樣就實(shí)現(xiàn)了進(jìn)程間通信。

管道使用的過(guò)程中可能會(huì)面臨問(wèn)題有：緩沖區(qū)的溢出，即當(dāng)要寫(xiě)入的數(shù)據(jù)大于緩沖區(qū)大小時(shí)，數(shù)據(jù)的丟失；阻塞問(wèn)題，讀寫(xiě)進(jìn)程在未滿足自身讀寫(xiě)要求時(shí)，可能會(huì)陷入死等狀態(tài)；還有管道破裂，即讀寫(xiě)進(jìn)程關(guān)閉不一致的情況；以及數(shù)據(jù)寫(xiě)入可能不保證原子性等等。文獻(xiàn)[13]提出了一種建模方法，本文針對(duì)其中的疏漏和不完善進(jìn)行了研究和改進(jìn)。

2.2 管道的建模

根據(jù)管道通信思想和源代碼的研讀，結(jié)合SPIN的使用特點(diǎn)，用有限狀態(tài)自動(dòng)機(jī)（FSA）描述模型。將管道、管道讀端以及寫(xiě)端看作3個(gè)實(shí)體，建立3個(gè)相應(yīng)的FSA，3個(gè)實(shí)體的交互，必然涉及到消息傳遞以及共享變量狀態(tài)改變，加上遷移條件的復(fù)雜性和耦合性，加大了建模的難度。文獻(xiàn)[13]中的模型存在如下等問(wèn)題：只使用了全局變量，遷移關(guān)系不完整，模型粒度不夠細(xì)化以及模型耦合關(guān)系復(fù)雜，現(xiàn)介紹另外一種改進(jìn)方案。

2.2.1 管道模型

在Linux中，管道的實(shí)現(xiàn)并沒(méi)有使用專門(mén)的數(shù)據(jù)結(jié)構(gòu)，而是借助了文件系統(tǒng)的file結(jié)構(gòu)和虛擬文件系統(tǒng)的索引節(jié)點(diǎn)inode。在此不展開(kāi)探討，僅僅對(duì)其抽象狀態(tài)進(jìn)行討論。管道通過(guò)系統(tǒng)調(diào)用pipe（）創(chuàng)建后，可進(jìn)行讀寫(xiě)操作，此時(shí)通過(guò)同步管道內(nèi)容管道進(jìn)行進(jìn)程間通信。在此期間，管道狀態(tài)可能是寫(xiě)狀態(tài)或者是讀狀態(tài)，而且在讀寫(xiě)端都未正式結(jié)束前，管道的狀態(tài)可能在兩個(gè)狀態(tài)間相互轉(zhuǎn)化。當(dāng)讀者或者寫(xiě)者結(jié)束時(shí)，管道進(jìn)入預(yù)關(guān)閉狀態(tài)，直到?jīng)]有讀者和寫(xiě)者，管道正式關(guān)閉。期間，若讀者提前退出，寫(xiě)者還未完成，則管道破裂。如果缺少了管道讀寫(xiě)狀態(tài)這一相互轉(zhuǎn)化的重要過(guò)程，也就是說(shuō)，管道創(chuàng)建以后只能進(jìn)行單一的讀或者寫(xiě)，這與實(shí)際情況是不符合的。

同時(shí)，盡管單獨(dú)把管道抽象成為一個(gè)實(shí)體，但其狀態(tài)變遷主要是依據(jù)讀寫(xiě)端的狀態(tài)變化完成，而不是管道主動(dòng)變遷的結(jié)果，因此讀寫(xiě)端的操作指令應(yīng)當(dāng)存在讀寫(xiě)端所代表實(shí)體中，而不是作為管道狀態(tài)的觸發(fā)條件。這樣的設(shè)計(jì)使實(shí)體間交互關(guān)系更加清楚，耦合性降低，同時(shí)也更符合設(shè)計(jì)邏輯。具體的過(guò)程見(jiàn)圖3所示。

圖3 管道模型

2.2.2 管道讀端

如果某個(gè)進(jìn)程要讀取管道中的數(shù)據(jù)，那么該進(jìn)程應(yīng)當(dāng)及時(shí)關(guān)閉fd[1]，以避免意外錯(cuò)誤的發(fā)生。讀端進(jìn)程通過(guò)調(diào)用read（）系統(tǒng)調(diào)用讀取管道內(nèi)容，讀端實(shí)體進(jìn)入READ狀態(tài)，此時(shí)分兩種情況，阻塞方式（NOBLOCK==0）和非阻塞方式讀?。∟OBLOCK==1）。

阻塞方式下：

1）如果管道中有數(shù)據(jù)（len>0）并且請(qǐng)求數(shù)據(jù)rdata不為0時(shí)，read操作時(shí)返回能夠讀取到的字節(jié)數(shù)。請(qǐng)求數(shù)據(jù)大于管道容量的，則返回管道中現(xiàn)有所有數(shù)據(jù)len；若請(qǐng)求字節(jié)數(shù)不大于管道容量，則返回現(xiàn)有所有數(shù)據(jù)或者請(qǐng)求的字節(jié)數(shù)；

2）如果管道中數(shù)據(jù)為0并且請(qǐng)求數(shù)據(jù)不為0時(shí)，若寫(xiě)端文件描述符未關(guān)閉則進(jìn)入等待狀態(tài)WAIT；

3）若管道中數(shù)據(jù)為0，寫(xiě)端文件描述符關(guān)閉，則返回0，進(jìn)入結(jié)束狀態(tài)FINISH；

4）阻塞等待的讀端進(jìn)程在管道有數(shù)據(jù)寫(xiě)入時(shí)再次進(jìn)入讀取狀態(tài)READ；

5）當(dāng)請(qǐng)求數(shù)據(jù)讀取完成后，進(jìn)入完成FINISH狀態(tài)。

非阻塞方式下：

1）如果管道中有數(shù)據(jù)并且請(qǐng)求數(shù)據(jù)不為0時(shí)，read操作時(shí)返回能夠讀取到的字節(jié)數(shù)；

2）若管道中數(shù)據(jù)為0，若管道寫(xiě)端被關(guān)閉，則返回0；若寫(xiě)端未關(guān)閉則返回-1；進(jìn)入FINISH狀態(tài)。

讀取結(jié)束，文件描述符關(guān)閉后，讀者計(jì)數(shù)器置0。具體的變遷過(guò)程如圖4所示。

圖4 管道讀端模型

2.2.3 管道寫(xiě)端

因?yàn)榫彌_區(qū)大小固定，管道寫(xiě)端的情況相對(duì)更加復(fù)雜。寫(xiě)進(jìn)程寫(xiě)入數(shù)據(jù)前需要關(guān)閉讀端，即close（fields[0]）。當(dāng)寫(xiě)進(jìn)程向管道中寫(xiě)入時(shí)，它利用標(biāo)準(zhǔn)的庫(kù)函數(shù)write（），系統(tǒng)根據(jù)庫(kù)函數(shù)傳遞的文件描述符，可找到該文件的file結(jié)構(gòu)。file結(jié)構(gòu)中指定了用來(lái)進(jìn)行寫(xiě)操作的函數(shù)（即寫(xiě)入函數(shù)）地址，同時(shí)需要滿足管道沒(méi)有被讀進(jìn)程占用。寫(xiě)進(jìn)程進(jìn)入數(shù)據(jù)寫(xiě)入狀態(tài)時(shí)，同樣分為阻塞和非阻塞兩種情況。

阻塞情況下：

1）只有緩沖區(qū)未滿的情況下，才能寫(xiě)入數(shù)據(jù)。當(dāng)寫(xiě)入數(shù)據(jù)wdata小于管道總長(zhǎng)度buf時(shí)，保證寫(xiě)入的原子性atomic，如果此時(shí)當(dāng)前可容納長(zhǎng)度小于寫(xiě)入數(shù)據(jù)時(shí)，寫(xiě)進(jìn)程進(jìn)入阻塞狀態(tài)WAIT，直到可以一次性寫(xiě)入；而當(dāng)寫(xiě)入數(shù)據(jù)大于管道總長(zhǎng)度時(shí)，不再保證寫(xiě)入過(guò)程的原子性，只要管道未滿，就寫(xiě)入數(shù)據(jù)，否則進(jìn)入阻塞狀態(tài)WAIT直到數(shù)據(jù)寫(xiě)完；

2）當(dāng)數(shù)據(jù)寫(xiě)入完畢，進(jìn)入FINISH狀態(tài)；

非阻塞情況下：

1）同樣也只有在管道未滿狀態(tài)下寫(xiě)入數(shù)據(jù)。當(dāng)寫(xiě)入數(shù)據(jù)wdata小于管道總長(zhǎng)度buf時(shí)，保證寫(xiě)入原子性，如果當(dāng)前可容納長(zhǎng)度大于寫(xiě)入長(zhǎng)度，則一次性寫(xiě)入，否則直接返回；

2）當(dāng)寫(xiě)入數(shù)據(jù)wdata大于管道總長(zhǎng)度buf時(shí)，若管道未滿，則寫(xiě)入可容納數(shù)據(jù)；若管道已滿則返回錯(cuò)誤；

在寫(xiě)入過(guò)程中，如果讀端完畢，關(guān)閉了文件描述符，則管道宣布破裂，產(chǎn)生信號(hào)SIGPIPE，返回-1。具體如圖5所示。

圖5 管道寫(xiě)端模型

2.2.4 模型的Promela描述

3個(gè)實(shí)體分別為進(jìn)程

各進(jìn)程初始狀態(tài)分別為

對(duì)用到的狀態(tài)作枚舉說(shuō)明

mtype={UNCREATED， CREATED， IsREAD，WRITTEN，ReadyCLOSE，BROKEN，CLOSE，UNWRITE，UNREAD，READ，WRITE，WAIT，F(xiàn)INISH}。

限于篇幅，同樣以管道部分Promela代碼為例，如圖6。新的建模方法中，管道部分加入了WRITTEN和READ狀態(tài)的相互轉(zhuǎn)化，同時(shí)剝離了管道和讀寫(xiě)端的操作聯(lián)系，狀態(tài)遷移僅由讀寫(xiě)端狀態(tài)和文件描述符狀態(tài)（讀寫(xiě)端計(jì)數(shù)）給出，如下：

同時(shí)由于管道狀態(tài)與讀寫(xiě)端進(jìn)程是同步關(guān)系，定義消息通道

mtype為枚舉類型，代表讀寫(xiě)端狀態(tài)；byte代表讀寫(xiě)端計(jì)數(shù)，即文件描述符。這樣的做法使管道狀態(tài)與讀寫(xiě)端進(jìn)程更能保持同步變化，比單純用全局變量更加精確，全局變量在SPIN中并不能保證同步。

對(duì)讀寫(xiě)端，為了減少狀態(tài)數(shù)，read和write操作返回值不同的情況將由打印信息printf（）給出，但都?xì)w為FINISH狀態(tài)。提高了程序可讀性，減少了模型檢測(cè)過(guò)程中系統(tǒng)的存儲(chǔ)狀態(tài)數(shù)，從而模型的復(fù)雜程度也得到簡(jiǎn)化。

增加和細(xì)化的遷移條件，使新模型更加完善；對(duì)原建模方法當(dāng)中的錯(cuò)誤遷移條件進(jìn)行了勘誤，如讀寫(xiě)端進(jìn)程是先結(jié)束，再關(guān)閉文件描述符，計(jì)數(shù)減少。

圖6 管道Promela部分代碼

3 實(shí)驗(yàn)結(jié)果分析及改進(jìn)

實(shí)驗(yàn)中，屬性用LTL表達(dá)式進(jìn)行描述，作為SPIN的輸入。

1）首先，是其有界性。即管道數(shù)據(jù)長(zhǎng)度len，不能超過(guò)管道總長(zhǎng)度buf，否則將會(huì)導(dǎo)致緩沖區(qū)溢出。用 ltl公式描述為 ltl p1{[]（len ＜ =buf）}，[]表示always。檢測(cè)結(jié)果表明性質(zhì)滿足。

圖7 ltl屬性驗(yàn)證

2）其次，驗(yàn)證讀寫(xiě)端不能同時(shí)占用管道，即讀端狀態(tài)為READ，寫(xiě)端狀態(tài)為WRITE。用ltl公式描述 為 ltl p2{[]!（Reader_State==READ&&Writer_State==WRITE）}。

檢驗(yàn)的結(jié)果表明，系統(tǒng)不滿足性質(zhì)，經(jīng)過(guò)反例查驗(yàn)，Reader_State==READ和Writer_State==WRITE可以同時(shí)成立，這與實(shí)際情況并不相符。原因在于同步機(jī)制，內(nèi)核會(huì)利用一定的機(jī)制同步對(duì)管道的訪問(wèn)，為此，內(nèi)核使用了鎖、等待隊(duì)列和信號(hào)。而本方法在管道到讀寫(xiě)進(jìn)程狀態(tài)只是使用了全局變量，致使讀寫(xiě)端進(jìn)程狀態(tài)沒(méi)有得到更新，為了更好的模擬實(shí)際情況，給出改進(jìn)措施：

a.增加同步通道

這樣管道狀態(tài)變化可以及時(shí)與讀寫(xiě)進(jìn)程通信，通知讀寫(xiě)進(jìn)程。實(shí)際上，管道狀態(tài)和讀寫(xiě)進(jìn)程狀態(tài)是互相制約，同步轉(zhuǎn)換的。

b.為讀寫(xiě)端實(shí)體各增加一個(gè)PAUSE狀態(tài)，與WAIT狀態(tài)區(qū)分，以讀端為例

圖8 改進(jìn)讀端模型

3）最后，通過(guò)更改初始參數(shù)，模擬不同的情況，驗(yàn)證可終止性，得到系統(tǒng)不同的結(jié)束狀態(tài)。也可用ltl 公 式 {＜ >（Reader_State == FINISH &&Writer_State==FINISH&&Pipe_State==CLOSE）}來(lái)檢驗(yàn)。當(dāng)違反屬性時(shí)，SPIN生成反例trail文件，可以沿錯(cuò)誤路徑再次進(jìn)行模擬，得到反例情況。

SPIN模擬輸出的結(jié)果格式如圖9所示，具體所有結(jié)果列于表1。

圖9 SPIN模擬輸出結(jié)果

表1 各實(shí)體終止?fàn)顟B(tài)

第一種情況代表管道讀寫(xiě)端正確讀?。ɑ蜃x取實(shí)際可讀數(shù)據(jù)）和寫(xiě)入數(shù)據(jù)后關(guān)閉；

第二種情況代表寫(xiě)端寫(xiě)入數(shù)據(jù)時(shí)，讀端關(guān)閉，管道宣布破裂；

第三種情況表明管道以非阻塞形式打開(kāi)，但管道為空，讀者返回-1；

第四種情況表明管道以非阻塞形式打開(kāi)，寫(xiě)入數(shù)據(jù)大于緩沖區(qū)總長(zhǎng)度且管道已滿或者寫(xiě)入數(shù)據(jù)小于緩沖區(qū)長(zhǎng)度但管道不足以容納；

第五種情況表明管道以阻塞形式打開(kāi)，寫(xiě)端寫(xiě)入完成，但讀端進(jìn)入了等待讀取數(shù)據(jù)的情況。實(shí)際上讀取進(jìn)程也可能工作得比寫(xiě)進(jìn)程快，當(dāng)寫(xiě)進(jìn)程還未關(guān)閉前，讀進(jìn)程讀空管道數(shù)據(jù)進(jìn)入了等待狀態(tài)，只有等待新的數(shù)據(jù)被寫(xiě)入。這種情況對(duì)應(yīng)于實(shí)際編程中打開(kāi)了文件描述符，而操作結(jié)束后，忘記close的情況，應(yīng)當(dāng)引起注意。

4 結(jié) 論

本文基于實(shí)際工作中的測(cè)試需要，對(duì)操作系統(tǒng)驗(yàn)證方法進(jìn)行了調(diào)研。簡(jiǎn)要介紹了形式化方法中的模型檢測(cè)，并對(duì)模型檢測(cè)工具SPIN及其編程語(yǔ)言Promela進(jìn)行了詳細(xì)描述?；赟PIN，對(duì)Linux進(jìn)程間通信手段之一的管道進(jìn)行了建模分析，對(duì)前人有關(guān)研究工作進(jìn)行了改進(jìn)、細(xì)化和補(bǔ)充完善。希望能夠拋磚引玉，對(duì)操作系統(tǒng)驗(yàn)證工作有所幫助和啟發(fā)。