彭 寒，曹?chē)?guó)震，吳曉葵

(西安航空學(xué)院 a.計(jì)算機(jī)學(xué)院；b.教務(wù)處，西安 710077)

0 引言

綜合模塊化航空電子架構(gòu)(Integrated Modular Avionics，IMA)已成為當(dāng)今航空、航天計(jì)算機(jī)的主流架構(gòu)，其主要目標(biāo)是實(shí)現(xiàn)分區(qū)操作系統(tǒng)，支持多個(gè)系統(tǒng)的時(shí)間分區(qū)和空間分區(qū)，以達(dá)到最大的資源利用率，減輕機(jī)載設(shè)備重量，減小飛機(jī)體積。機(jī)載分區(qū)操作系統(tǒng)為應(yīng)用程序提供時(shí)空隔離的保障，從而實(shí)現(xiàn)故障隔離，避免故障傳播，并為不同安全級(jí)別的分系統(tǒng)提供物理上的隔離機(jī)制。為實(shí)現(xiàn)分區(qū)操作系統(tǒng)的標(biāo)準(zhǔn)化，美國(guó)航空無(wú)線電公司提出了機(jī)載分區(qū)操作系統(tǒng)實(shí)現(xiàn)規(guī)范——ARINC 653標(biāo)準(zhǔn)，旨在規(guī)定分區(qū)操作系統(tǒng)和機(jī)載應(yīng)用程序之間的接口，以支持機(jī)載安全關(guān)鍵系統(tǒng)的開(kāi)發(fā)認(rèn)證和驗(yàn)證。ARINC 653標(biāo)準(zhǔn)經(jīng)過(guò)不斷的改進(jìn)和完善，已經(jīng)覆蓋了分區(qū)操作系統(tǒng)的核心服務(wù)、擴(kuò)展服務(wù)、文件系統(tǒng)、測(cè)試驗(yàn)證標(biāo)準(zhǔn)等各個(gè)方面。以ARINC 653標(biāo)準(zhǔn)為依據(jù)的各種分區(qū)操作系統(tǒng)也已得到了廣泛應(yīng)用，例如，VxWorks653、INTEGRITY-178B，LynxOS-178，PikeOS和開(kāi)源軟件POK及 Xtratum。

分區(qū)操作系統(tǒng)作為機(jī)載系統(tǒng)的重要基礎(chǔ)軟件，對(duì)其安全性、可靠性有著嚴(yán)苛的要求。由于分區(qū)操作系統(tǒng)的復(fù)雜性，其安全性往往難以通過(guò)測(cè)試和仿真來(lái)保證，根本原因在于軟件工程中的需求分析、設(shè)計(jì)和驗(yàn)證通常采用非形式化語(yǔ)言來(lái)完成，而這種方式存在很大的二義性、模糊性，缺乏嚴(yán)格的數(shù)學(xué)證明。對(duì)于安全關(guān)鍵的機(jī)載分區(qū)操作系統(tǒng)，需要一種嚴(yán)格的、可靠的、實(shí)用的方法實(shí)現(xiàn)對(duì)復(fù)雜系統(tǒng)的管理。因此，在各種航空軟件安全性規(guī)范(如DO-178C)中，已經(jīng)明確提出了要采用形式化方法對(duì)嵌入式系統(tǒng)進(jìn)行建模和驗(yàn)證。本文在國(guó)內(nèi)外機(jī)載分區(qū)操作系統(tǒng)形式化建模及驗(yàn)證研究工作的基礎(chǔ)上進(jìn)行了分析總結(jié)，指出了當(dāng)前該領(lǐng)域存在的問(wèn)題，并提出了新的發(fā)展思路。

1 分區(qū)操作系統(tǒng)形式化建模與驗(yàn)證研究現(xiàn)狀

分區(qū)操作系統(tǒng)的形式化建模通常是根據(jù)建模者的經(jīng)驗(yàn)，先設(shè)計(jì)抽象規(guī)約，然后逐步精化為底層模型，最終得到最貼近具體實(shí)現(xiàn)的精化模型。當(dāng)前分區(qū)操作系統(tǒng)的形式化建模的研究包括分區(qū)操作系統(tǒng)的內(nèi)核建模研究和分區(qū)操作系統(tǒng)規(guī)范的建模研究。

1.1 分區(qū)操作系統(tǒng)內(nèi)核建模

Craig[1]使用自動(dòng)化的建模與驗(yàn)證工具Z Notations 設(shè)計(jì)并精化了一個(gè)較為完整的操作系統(tǒng)的內(nèi)核，并證明了可以將其直接轉(zhuǎn)換為C語(yǔ)言的可執(zhí)行代碼；而后，又進(jìn)一步設(shè)計(jì)和精化了一個(gè)分區(qū)操作系統(tǒng)的內(nèi)核，該內(nèi)核提供了分區(qū)操作系統(tǒng)的大部分的功能。Craig使用定理證明方法對(duì)幾個(gè)內(nèi)核屬性進(jìn)行了基本的驗(yàn)證，Craig設(shè)計(jì)的分區(qū)操作系統(tǒng)的形式化規(guī)約是一個(gè)較為完整的規(guī)約，其精化的級(jí)別已經(jīng)達(dá)到了可以直接轉(zhuǎn)換為C代碼或者Ada代碼的程度。但是Craig的設(shè)計(jì)中沒(méi)有建立分區(qū)內(nèi)進(jìn)程的模型，另外，對(duì)于硬件設(shè)備的建模較為簡(jiǎn)略，其形式化規(guī)約和正確性證明都是完全靠人工完成的。

Velykis在Craig研究的基礎(chǔ)上，考慮了更多的安全性需求， 使用自動(dòng)化的建模與驗(yàn)證工具Z Notations完成了分區(qū)操作系統(tǒng)的進(jìn)一步的規(guī)約和驗(yàn)證[2]，使用Z / Eves自動(dòng)定理證明器對(duì)其形式化規(guī)約進(jìn)行了驗(yàn)證，消除了Craig的模型中的語(yǔ)法錯(cuò)誤，并驗(yàn)證了其API的可行性和健壯性，其改進(jìn)的分區(qū)操作系統(tǒng)的形式化模型是完全使用定理證明器自動(dòng)證明的。但是，Velykis的形式化規(guī)約中沒(méi)有涉及分區(qū)隔離方面的證明，其改進(jìn)的的形式化模型側(cè)重于分區(qū)操作系統(tǒng)內(nèi)核中的核心數(shù)據(jù)結(jié)構(gòu)，例如進(jìn)程表、隊(duì)列和調(diào)度程序，主要是改進(jìn)了 Craig的調(diào)度器模型，并將調(diào)度器的某些行為屬性(如調(diào)度器死鎖分析)從非形式化的需求轉(zhuǎn)換為數(shù)學(xué)不變量來(lái)完成了證明。而對(duì)于其他組件，如消息傳遞或內(nèi)存管理，則沒(méi)有使用自動(dòng)證明。

Critical軟件公司的Andre使用形式化建模語(yǔ)言—B語(yǔ)言設(shè)計(jì)了一個(gè)安全的分區(qū)操作系統(tǒng)內(nèi)核(secure partitioning kernel ,SPK)的形式化模型。其研究成果首先是完整的開(kāi)發(fā)了SPK的頂層模型，完成系統(tǒng)的架構(gòu)設(shè)計(jì)，并用ProB[3]工具進(jìn)行了仿真和驗(yàn)證。頂層的SPK抽象模型由內(nèi)存管理、調(diào)度、內(nèi)核通信、流策略、時(shí)鐘模型等組成。而后，經(jīng)過(guò)驗(yàn)證的頂層模型可以精化為完全形式化的精化SPK，并最終精化到可以從其自動(dòng)生成C代碼的級(jí)別，這個(gè)精化過(guò)程是在Atelier B工具的協(xié)助下完成的。

Kawamorita 等人也應(yīng)用B語(yǔ)言開(kāi)發(fā)了安全的嵌入式設(shè)備上的分區(qū)操作系統(tǒng)內(nèi)核OS-K，并在Intel的IA-32架構(gòu)上搭建了該操作系統(tǒng)的原型[4]。Kawamorita使用B語(yǔ)言作為形式化模型的開(kāi)發(fā)工具，并用Spin工具驗(yàn)證了該模型的屬性，同時(shí)，他使用B4free工具自動(dòng)驗(yàn)證了模型的正確性和一致性。最終的分區(qū)操作系統(tǒng)內(nèi)核提供了幾個(gè)核心的功能：分區(qū)管理、分區(qū)間通信、分區(qū)間通信的訪問(wèn)控制、內(nèi)存管理、定時(shí)器管理、處理器調(diào)度、設(shè)備驅(qū)動(dòng)程序操作和中斷處理的I/O中斷同步。

Phelps等人使用Alloy語(yǔ)言設(shè)計(jì)了一個(gè)安全的分區(qū)操作系統(tǒng)的安全策略的形式化模型和頂級(jí)規(guī)約，并用分析工具驗(yàn)證了該規(guī)約的一致性。該規(guī)約精化了分區(qū)間信息流策略模型，并且使用狀態(tài)轉(zhuǎn)換系統(tǒng)建立了兩個(gè)相互連接的分離的子系統(tǒng)，初始化時(shí)的子系統(tǒng)和運(yùn)行時(shí)子系統(tǒng)。

Martin等人使用形式化規(guī)約開(kāi)發(fā)軟件SPECWARE開(kāi)發(fā)了MASK分區(qū)操作系統(tǒng)，并進(jìn)行了三次精化[5]，其抽象規(guī)約主要涉及內(nèi)核數(shù)據(jù)結(jié)構(gòu)的規(guī)約，而最終的底層規(guī)約被手工翻譯成C源代碼。

為了保證Xenon分區(qū)操作系統(tǒng)的信息流安全性，F(xiàn)reitas和McDermott使用Circus建模語(yǔ)言建立了Xenon分區(qū)操作系統(tǒng)的形式化模型[6]。Murray 等人用Isabelle/HOL建模語(yǔ)言完成了對(duì)安全的分區(qū)操作系統(tǒng)內(nèi)核seL4的建模和驗(yàn)證，他們將seL4的規(guī)范用于驗(yàn)證分區(qū)操作系統(tǒng)的信息流安全性，規(guī)范中定義了基于分區(qū)的輪轉(zhuǎn)調(diào)度策略，給每個(gè)分區(qū)分配了固定的時(shí)間窗口。歐盟EURO-MILS項(xiàng)目以PikeOS操作系統(tǒng)的精確建模和安全策略建模為目標(biāo)，用Isabelle/HOL建模語(yǔ)言設(shè)計(jì)了一個(gè)通用的分區(qū)操作系統(tǒng)CISK(Controlled Interruptible Separation Kernel)的形式化模型，該模型包含了分區(qū)操作系統(tǒng)的幾個(gè)方面，例如中斷、分區(qū)之間的上下文切換和控制，其規(guī)約較為詳細(xì)，適用于工業(yè)系統(tǒng)的形式化驗(yàn)證。Sanan等人在基于歐洲航天局的IMA for Space項(xiàng)目中，用 Isabelle / HOL建模語(yǔ)言構(gòu)建了通用的分區(qū)操作系統(tǒng)內(nèi)核的功能模型和安全模型。該規(guī)范使用ARINC 653作為功能需求，為了服務(wù)于最終的軟件實(shí)現(xiàn)，也涉及到了硬件虛擬化、CPU定時(shí)器和內(nèi)存管理的模型。趙永望等人使用Isabelle / HOL建模語(yǔ)言設(shè)計(jì)了ARINC 653兼容的分區(qū)操作系統(tǒng)的頂層模型，其中考慮了ARINC 653的分區(qū)管理、分區(qū)調(diào)度和通信服務(wù)。

1.2 分區(qū)操作系統(tǒng)規(guī)范建模

由于分區(qū)操作系統(tǒng)規(guī)范的內(nèi)核接口規(guī)范中規(guī)定了內(nèi)核需要為應(yīng)用程序提供的核心服務(wù)，對(duì)分區(qū)操作系統(tǒng)規(guī)范的建模需求也日漸迫切，因?yàn)樾问交姆謪^(qū)操作系統(tǒng)接口模型能夠支持對(duì)分區(qū)應(yīng)用程序的形式化建模與驗(yàn)證。York大學(xué)的Gomes 用Circus建模語(yǔ)言建立了針對(duì)IMA系統(tǒng)的ARINC 653規(guī)范的形式化模型，Camara 等人對(duì)運(yùn)行在ARINC 653兼容的分區(qū)操作系統(tǒng)之上的應(yīng)用程序進(jìn)行了建模和驗(yàn)證[7]。北京航空航天大學(xué)的趙永望等人使用Event-B建模語(yǔ)言建立了ARINC 653第1部分的57項(xiàng)服務(wù)的系統(tǒng)功能的形式化模型，他們使用Event-B建模語(yǔ)言中的精化結(jié)構(gòu)將ARINC 653抽象模型逐步精化，并將ARINC 653的服務(wù)要求轉(zhuǎn)換為了底層模型。趙永望利用Event-B的邏輯推理的能力證明了該規(guī)范的三個(gè)隱藏的錯(cuò)誤和不完整之處，是一個(gè)將Event-B建模語(yǔ)言用于復(fù)雜系統(tǒng)建模與驗(yàn)證的很好的范例。

雖然目前已有對(duì)分區(qū)操作系統(tǒng)的形式化建模的研究，但是還沒(méi)有直接從某個(gè)分區(qū)操作系統(tǒng)的形式化模型直接生成可執(zhí)行代碼的報(bào)告。

2 分區(qū)操作系統(tǒng)的形式化驗(yàn)證

分區(qū)操作系統(tǒng)的形式化驗(yàn)證通常是從已有的操作系統(tǒng)代碼中抽象出形式化模型，并驗(yàn)證這個(gè)抽象模型的各種屬性。分區(qū)操作系統(tǒng)的形式化驗(yàn)證主要包括對(duì)時(shí)間隔離能力和空間隔離能力的驗(yàn)證，其中空間隔離能力指的是數(shù)據(jù)的隔離，也就是數(shù)據(jù)存儲(chǔ)和數(shù)據(jù)通信的分離，即不能有非法的、不安全的訪問(wèn)和分區(qū)間的故障傳播。分區(qū)的時(shí)間隔離能力則確保了共享資源為分區(qū)中的軟件提供的服務(wù)不會(huì)受到其他分區(qū)中的軟件的影響，包括計(jì)算資源的性能、調(diào)度資源的速率、延遲、抖動(dòng)和持續(xù)時(shí)間。

2.1 空間隔離能力驗(yàn)證

Baumann 等人在一個(gè)航空電子項(xiàng)目的子工程中用VCC驗(yàn)證工具驗(yàn)證了PikeOS分區(qū)操作系統(tǒng)源代碼的所有系統(tǒng)調(diào)用功能，也就是內(nèi)核提供給應(yīng)用程序的核心服務(wù)的正確性。他們提出了頂層抽象模型和底層實(shí)現(xiàn)的操作系統(tǒng)及應(yīng)用程序構(gòu)成的系統(tǒng)之間的模擬關(guān)系定理，并識(shí)別出了為保證分區(qū)操作系統(tǒng)內(nèi)核的整體正確性而需要所有組件所具備的屬性。因?yàn)榻⒃赑ikeOS分區(qū)操作系統(tǒng)源代碼上的安全關(guān)鍵系統(tǒng)依賴(lài)于空間分離機(jī)制的正確實(shí)現(xiàn)，所以對(duì)它的驗(yàn)證必須考慮內(nèi)存隔離的正確性。因此，Baumann等人使用VCC工具對(duì)PikeOS分區(qū)操作系統(tǒng)的關(guān)鍵組件，即內(nèi)存管理器進(jìn)行了源代碼的級(jí)別的驗(yàn)證。

Richards對(duì)格林希爾公司的商業(yè)化分區(qū)操作系統(tǒng)INTEGRITY-178B進(jìn)行了安全性驗(yàn)證[8]，其驗(yàn)證考慮了五個(gè)要素：(1)描述系統(tǒng)相關(guān)安全屬性的形式化規(guī)約；(2)系統(tǒng)功能性接口的形式化表示；(3)系統(tǒng)高層設(shè)計(jì)的半形式化表示和抽象表示；(4)系統(tǒng)低層設(shè)計(jì)的半形式化的、詳細(xì)的表示；(5)用來(lái)表示上述四個(gè)要素對(duì)之間的對(duì)應(yīng)關(guān)系的模型。該系統(tǒng)被建模為狀態(tài)轉(zhuǎn)換系統(tǒng)，它接收系統(tǒng)的當(dāng)前狀態(tài)以及任何外部輸入作為輸入，并產(chǎn)生新的系統(tǒng)狀態(tài)以及任何外部輸出。Richards采用這種方式驗(yàn)證了INTEGRITY-178B的高層模型信息流安全性，系統(tǒng)的低層設(shè)計(jì)采用ACL2定理證明器建模，并保證了ACL2模型與C代碼的對(duì)應(yīng)性。

基于ARM的嵌入式分區(qū)操作系統(tǒng)PROSPER的內(nèi)核由150行匯編代碼和600行C代碼組成，Dam通過(guò)證明抽象規(guī)約和內(nèi)核二進(jìn)制代碼之間的相互模擬關(guān)系，對(duì)PROSPER的信息流安全性進(jìn)行了形式化驗(yàn)證，其系統(tǒng)模型僅考慮分別在兩個(gè)獨(dú)立的特殊ARMv7機(jī)器上執(zhí)行的兩個(gè)分區(qū)，分區(qū)間通過(guò)異步消息傳遞進(jìn)行通信，最終驗(yàn)證了除了通過(guò)指定的通信通道之外，分區(qū)之間不會(huì)有任何直接或間接地影響。具體做法是確保除了通過(guò)顯式使用預(yù)先指定的通道來(lái)實(shí)現(xiàn)通信外，分區(qū)間無(wú)法通過(guò)讀/寫(xiě)其他分區(qū)的內(nèi)存、寄存器的內(nèi)容來(lái)訪問(wèn)其它分區(qū)。

2.2 時(shí)間隔離能力驗(yàn)證

時(shí)間隔離需要用分區(qū)操作系統(tǒng)的調(diào)度器來(lái)實(shí)現(xiàn)，因?yàn)樗?fù)責(zé)將處理器時(shí)間分配給分區(qū)。根據(jù)ARINC 653標(biāo)準(zhǔn)，時(shí)間分離需要兩級(jí)調(diào)度器，分別為分區(qū)級(jí)調(diào)度器和進(jìn)程級(jí)調(diào)度器。

霍尼韋爾動(dòng)態(tài)執(zhí)行操作系統(tǒng)(Dynamic Enforcement Operating System，DEOS)是一個(gè)基于微內(nèi)核的實(shí)時(shí)操作系統(tǒng)，通過(guò)在進(jìn)程級(jí)別提供空間隔離和在線程級(jí)提供時(shí)間分區(qū)來(lái)支持靈活的IMA應(yīng)用程序。NASA與霍尼韋爾合作，將DEOS的調(diào)度內(nèi)核的核心部分包含10個(gè)類(lèi)，超過(guò)1000行的C++代碼翻譯成Promela，并在Spin模型檢測(cè)工具中進(jìn)行了驗(yàn)證[9]。他們使用兩種方法來(lái)分析DEOS內(nèi)核中的時(shí)間隔離屬性。第一種方法是建立程序變量的斷言以識(shí)別潛在的錯(cuò)誤。如果模型檢查器發(fā)現(xiàn)了斷言背離，則可以仿真所報(bào)告的錯(cuò)誤的執(zhí)行路徑，并且可以確定這個(gè)路徑是否真的是錯(cuò)誤的執(zhí)行路徑。第二種方法是使用LTL表達(dá)的活性屬性Idle Execution，其形式為(beginperiod->(！endperiod U idle))。這個(gè)活性屬性表示如果系統(tǒng)中有時(shí)間松弛(即主線程沒(méi)有100%的CPU利用率)，則空閑線程應(yīng)該在每個(gè)最長(zhǎng)的周期內(nèi)運(yùn)行，這是時(shí)間隔離的必要條件。該系統(tǒng)的大小和復(fù)雜性限制了它們一次只能分析一個(gè)配置。為了克服這個(gè)局限性，Ha等人使用定理證明的方法將DEOS的驗(yàn)證推廣到任意配置，利用PVS定理證明器來(lái)分析DEOS調(diào)度器。他們使用離散時(shí)間狀態(tài)轉(zhuǎn)換系統(tǒng)對(duì)PVS中的調(diào)度器的操作和DEOS的執(zhí)行時(shí)間線建模，時(shí)間隔離屬性被建模為狀態(tài)集合上的謂詞，并被證明適用于所有可達(dá)到的狀態(tài)，整個(gè)理論模型共有1648行PVS代碼和212個(gè)引理。除了時(shí)間隔離不變量的歸納證明之外，他們還使用基于特征模型的技術(shù)來(lái)模擬狀態(tài)轉(zhuǎn)換系統(tǒng)并確定歸納不變量，這種技術(shù)對(duì)于漸增復(fù)雜度的系統(tǒng)的增量式的定理證明非常適用。

Asberg等人使用時(shí)間任務(wù)自動(dòng)機(jī)對(duì)WindRiver的分區(qū)操作系統(tǒng)VxWorks進(jìn)行建模，并使用Times工具對(duì)其進(jìn)行了驗(yàn)證。他們使用時(shí)間任務(wù)自動(dòng)機(jī)建立了全局調(diào)度器、分區(qū)內(nèi)本地調(diào)度器和事件處理程序的模型，用事件處理程序模型將全局調(diào)度器和分區(qū)個(gè)數(shù)的變化解耦。Asberg用時(shí)間計(jì)算樹(shù)邏輯TCTL建模了分區(qū)內(nèi)局部調(diào)度器和全局調(diào)度器應(yīng)滿足的安全性需求，例如“當(dāng)分區(qū)處于活動(dòng)狀態(tài)時(shí)，分區(qū)內(nèi)任務(wù)就緒隊(duì)列中優(yōu)先級(jí)最高的任務(wù)應(yīng)始終是服務(wù)器當(dāng)前正在運(yùn)行的任務(wù)”。

2.3 討論

通過(guò)對(duì)國(guó)內(nèi)外分區(qū)操作系統(tǒng)形式化建模與驗(yàn)證技術(shù)研究現(xiàn)狀的分析，我們可以發(fā)現(xiàn)，大多數(shù)對(duì)空間隔離能力進(jìn)行的建模和驗(yàn)證都采用了定理證明的方法，原因在于模型檢查方法由于其狀態(tài)空間爆炸問(wèn)題無(wú)法完整地驗(yàn)證操作系統(tǒng)的所有可能執(zhí)行路徑，并且很難用屬性建模語(yǔ)言(如LTL和CTL)表達(dá)空間隔離屬性。反之，驗(yàn)證時(shí)間隔離屬性時(shí)，通常會(huì)使用模型檢驗(yàn)方法，這是因?yàn)樵诟鞣N模型檢查器中可以很方便地表達(dá)時(shí)間屬性，例如UPPAAL工具中的時(shí)間自動(dòng)機(jī)。

3 現(xiàn)有建模及驗(yàn)證研究中存在的問(wèn)題

雖然國(guó)內(nèi)外研究人員已在分區(qū)操作系統(tǒng)建模及驗(yàn)證方面做了一定的工作，但是這些研究目前尚存在下述問(wèn)題。

3.1 驗(yàn)證工作的不充分性

目前分區(qū)操作系統(tǒng)驗(yàn)證的工作通常是對(duì)已有的操作系統(tǒng)代碼的“設(shè)計(jì)后驗(yàn)證”，所驗(yàn)證的模型僅僅是實(shí)際系統(tǒng)的一個(gè)抽象，只能體現(xiàn)系統(tǒng)的可能行為，而不是全部行為。這種方法最大的問(wèn)題在于必須保證抽象出來(lái)的形式化模型與原來(lái)的源代碼的行為是一致的，而事實(shí)上，無(wú)論這個(gè)抽象過(guò)程是自動(dòng)的還是人工的，都無(wú)法避免不一致性。因此，這些驗(yàn)證工作是不充分的。

3.2 建模與驗(yàn)證方法的單一性

目前已有的分區(qū)操作系統(tǒng)建模及驗(yàn)證方法主要側(cè)重于建?；蛘唑?yàn)證系統(tǒng)的某個(gè)方面的屬性，很少能夠完整地覆蓋多個(gè)方面的屬性建模和驗(yàn)證需求。例如，Event-B、B、Z等基于數(shù)據(jù)精化的建模語(yǔ)言主要注重于保證模型精化的一致性，而無(wú)法對(duì)各種時(shí)態(tài)邏輯屬性進(jìn)行驗(yàn)證。時(shí)間自動(dòng)機(jī)、狀態(tài)轉(zhuǎn)換系統(tǒng)等工具可以很方便的建模和驗(yàn)證模型的行為特性，而對(duì)于數(shù)據(jù)精化方面的支持則比較弱，缺乏同時(shí)考慮數(shù)據(jù)精化特性和行為屬性的形式化模型和驗(yàn)證研究。

3.3 缺乏對(duì)交互環(huán)境的建模與驗(yàn)證

當(dāng)前的分區(qū)操作系統(tǒng)的形式化模型并沒(méi)有區(qū)分“環(huán)境”和“系統(tǒng)”，基本上都是將環(huán)境和系統(tǒng)放到一起，構(gòu)成一個(gè)封閉的系統(tǒng)。所謂“環(huán)境”就是會(huì)和操作系統(tǒng)產(chǎn)生交互的系統(tǒng)，如硬件系統(tǒng)和應(yīng)用軟件。現(xiàn)有的研究成果或者是沒(méi)有考慮這些因素，或者是將這些因素作為了分區(qū)操作系統(tǒng)模型的一部分，混淆了系統(tǒng)所處的環(huán)境模型和系統(tǒng)本身的模型，這些模型對(duì)于驗(yàn)證規(guī)范和標(biāo)準(zhǔn)是可行的，但對(duì)于需要根據(jù)模型生成最終代碼的工程師來(lái)說(shuō)則是不可接受的。

4 分區(qū)操作系統(tǒng)建模及驗(yàn)證的新思路

針對(duì)當(dāng)前分區(qū)操作系統(tǒng)建模及驗(yàn)證的研究工作中存在的問(wèn)題，本文提出以下三種新的思路，以期對(duì)未來(lái)研究工作有所借鑒。

4.1 從“設(shè)計(jì)后驗(yàn)證”到“Correct-by-Construct”方法

傳統(tǒng)的形式化方法只考慮了軟件壽命周期的需求規(guī)約階段和最終的測(cè)試驗(yàn)證階段，而沒(méi)有控制中間的設(shè)計(jì)和實(shí)現(xiàn)過(guò)程。Correct-by-Construct方法是近年來(lái)學(xué)界所提倡的新的、更科學(xué)的形式化方法。其含義為“構(gòu)建即正確”，即軟件的正確性應(yīng)該是通過(guò)正確的“設(shè)計(jì)(構(gòu)建)”來(lái)保證的，而不是通過(guò)驗(yàn)證來(lái)保證。Correct-by-Construct方法能夠從需求規(guī)約開(kāi)始，逐步精化規(guī)約模型，得到設(shè)計(jì)模型，直到生成最終的實(shí)現(xiàn)代碼，并保證整個(gè)精化過(guò)程的正確性。對(duì)于安全關(guān)鍵的機(jī)載分區(qū)操作系統(tǒng)來(lái)說(shuō)，必須采用這種方法“構(gòu)建”出正確的分區(qū)操作系統(tǒng)。

4.2 從規(guī)約模型到契約模型

現(xiàn)有的分區(qū)操作系統(tǒng)模型未能區(qū)分系統(tǒng)模型和系統(tǒng)所處的“環(huán)境”的模型，完整的建模分區(qū)操作系統(tǒng)和其所處的“環(huán)境”的模型會(huì)讓模型的規(guī)模變得極為復(fù)雜也是不現(xiàn)實(shí)的。因此，可以采用契約式設(shè)計(jì)與驗(yàn)證的思路，建立系統(tǒng)和環(huán)境的“契約”，有效地分離系統(tǒng)模型和環(huán)境模型，即定義系統(tǒng)和環(huán)境之間的接口。只要分區(qū)操作系統(tǒng)滿足這個(gè)契約，就是可行的實(shí)現(xiàn)方案。在實(shí)際操作的過(guò)程中，可以建立底層硬件應(yīng)該滿足的行為的契約，甚至是分區(qū)操作系統(tǒng)的底層支撐操作系統(tǒng)所提供的接口模型作為分區(qū)操作系統(tǒng)的環(huán)境模型。

4.3 組合運(yùn)用多種形式化建模方法

形式化建模語(yǔ)言因其專(zhuān)用性的特點(diǎn)，很難同時(shí)考慮系統(tǒng)的多方面的屬性建模與驗(yàn)證。例如，某些建模語(yǔ)言主要擅長(zhǎng)建模系統(tǒng)的行為方面的屬性，而另一些建模語(yǔ)言則專(zhuān)注于時(shí)間屬性的建模。為應(yīng)對(duì)這個(gè)問(wèn)題，研究人員通常會(huì)根據(jù)實(shí)際需求對(duì)某些形式化建模語(yǔ)言進(jìn)行擴(kuò)充，使其能夠表達(dá)更多方面的屬性。但事實(shí)上是不存在能夠表達(dá)系統(tǒng)所有方面屬性的形式系統(tǒng)的，而且很多形式系統(tǒng)中有大量不需要的語(yǔ)法元素。一種比較靈活的且更為現(xiàn)實(shí)的做法是根據(jù)實(shí)際的系統(tǒng)建模與驗(yàn)證需求，組合運(yùn)用多種形式化方法，這樣，建模者只需要選擇合適的形式系統(tǒng)用來(lái)滿足建模和驗(yàn)證需求，就可以將研究重點(diǎn)轉(zhuǎn)向系統(tǒng)模型的構(gòu)建、精化和屬性驗(yàn)證上。

5 結(jié)語(yǔ)

本文通過(guò)分析國(guó)內(nèi)外關(guān)于機(jī)載分區(qū)操作系統(tǒng)建模及驗(yàn)證方面的研究成果，指出了其研究工作中存在著驗(yàn)證工作不充分性、建模與驗(yàn)證方法單一性、缺乏對(duì)交互環(huán)境的建模與驗(yàn)證等問(wèn)題，并針對(duì)這些問(wèn)題，提出了從“設(shè)計(jì)后驗(yàn)證”到“Correct-by-Construct”、從規(guī)約模型到契約模型、組合運(yùn)用多種形式化建模三種新的研究方法及解決方案，為進(jìn)一步開(kāi)展機(jī)載分區(qū)操作系統(tǒng)建模及驗(yàn)證工作提供了指南。