機載分區(qū)操作系統(tǒng)形式化建模及驗證研究

彭 寒，曹國震，吳曉葵

(西安航空學院 a.計算機學院；b.教務處，西安 710077)

0 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.1 空間隔離能力驗證

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

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

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

2.2 時間隔離能力驗證

時間隔離需要用分區(qū)操作系統(tǒng)的調(diào)度器來實現(xiàn)，因為它負責將處理器時間分配給分區(qū)。根據(jù)ARINC 653標準，時間分離需要兩級調(diào)度器，分別為分區(qū)級調(diào)度器和進程級調(diào)度器。

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

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

2.3 討論

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

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

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

3.1 驗證工作的不充分性

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

3.2 建模與驗證方法的單一性

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

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

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

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

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

4.1 從“設計后驗證”到“Correct-by-Construct”方法

傳統(tǒng)的形式化方法只考慮了軟件壽命周期的需求規(guī)約階段和最終的測試驗證階段，而沒有控制中間的設計和實現(xiàn)過程。Correct-by-Construct方法是近年來學界所提倡的新的、更科學的形式化方法。其含義為“構(gòu)建即正確”，即軟件的正確性應該是通過正確的“設計(構(gòu)建)”來保證的，而不是通過驗證來保證。Correct-by-Construct方法能夠從需求規(guī)約開始，逐步精化規(guī)約模型，得到設計模型，直到生成最終的實現(xiàn)代碼，并保證整個精化過程的正確性。對于安全關鍵的機載分區(qū)操作系統(tǒng)來說，必須采用這種方法“構(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)境”的模型會讓模型的規(guī)模變得極為復雜也是不現(xiàn)實的。因此，可以采用契約式設計與驗證的思路，建立系統(tǒng)和環(huán)境的“契約”，有效地分離系統(tǒng)模型和環(huán)境模型，即定義系統(tǒng)和環(huán)境之間的接口。只要分區(qū)操作系統(tǒng)滿足這個契約，就是可行的實現(xiàn)方案。在實際操作的過程中，可以建立底層硬件應該滿足的行為的契約，甚至是分區(qū)操作系統(tǒng)的底層支撐操作系統(tǒng)所提供的接口模型作為分區(qū)操作系統(tǒng)的環(huán)境模型。

4.3 組合運用多種形式化建模方法

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

5 結(jié)語

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