基于Event-B的SpaceOS2操作系統(tǒng)任務管理需求形式化建模與驗證

譚彥亮，楊 樺，喬 磊

(北京控制工程研究所，北京100190)

0 引言

操作系統(tǒng)是計算機系統(tǒng)的重要組成部分，管理著系統(tǒng)的硬件資源，是應用程序得以正確運行的基礎.操作系統(tǒng)的可靠依賴于內核的可靠，尤其像航天器這種安全攸關的系統(tǒng)，對嵌入式操作系統(tǒng)有極高的可靠性、安全性、正確性要求，因此對操作系統(tǒng)內核進行驗證是有必要的.

形式化方法可以幫助分析系統(tǒng)描述不一致、不明確或不完整的部分，通過邏輯推理可以驗證模型是否滿足需求規(guī)約，已成為公認的提高軟件質量、增強系統(tǒng)可靠性的有效方法.其基本過程是用形式化語言對系統(tǒng)進行描述，建立系統(tǒng)的形式化模型，這稱為形式化規(guī)約，之后采用模型檢測、定理證明等形式化驗證方法對模型進行驗證，保證模型的正確性.

采用形式化方法來驗證操作系統(tǒng)正確性由來已久，早在1980年，美國加州大學洛杉磯分校的Walker等［1］就對Unix的安全內核進行了形式化描述與驗證工作，Bevier［2］建立了內核形式模型，文獻［3］對操作系統(tǒng)規(guī)約進行了形式化描述.澳大利亞NICTA在2004年對操作系統(tǒng)內核L4開展了形式化驗證工作并發(fā)布了新一代嵌入式操作系統(tǒng)seL4，項目負責人Klein等［4］宣稱嵌入式安全操作系統(tǒng)seL4是第一個使用正規(guī)機器檢測證明(formal machinechecked proof)的通用操作系統(tǒng)，按照軟件可信度量標準CC標準的技術評價指標，seL4已經超越了EAL-7級水平.

當前對操作系統(tǒng)的形式化研究工作主要集中在對模型的描述與對其性質的驗證上，這在NICTA Workshop關于L4內核的多篇論文中都有具體體現(xiàn).

航天操作系統(tǒng)SpaceOS是由北京控制工程研究所研制的星載計算機嵌入式操作系統(tǒng)，在多個航天型號任務上得到了實際應用.其中SpaceOS2是第二代星載計算機操作系統(tǒng)，已經成功應用在探月工程嫦娥三號巡視器“玉兔號”月球車上.

本文使用Event-B［5］形式化方法對嵌入式操作系統(tǒng)SpaceOS2形式化地建立了一個任務需求的模型，需求提出的任務約束性質在Rodin［6］平臺上得到了驗證.

1 Event-B簡介

Event-B是一種基于狀態(tài)的形式化方法，其數(shù)學理論基礎是集合論和謂詞邏輯，常用于系統(tǒng)級的建模與分析.基于Eclipse的Rodin平臺為Event-B提供了形式化建模環(huán)境與自動化驗證的工具，同時有多種插件可以方便地驗證證明.

1.1 Event-B 模型

Event-B的模型是通過抽象狀態(tài)機(ASM，abstract state machine)來定義的，ASM使用變量來表示模型的狀態(tài)，定義事件來對其狀態(tài)進行操作.ASM通過自動機(machine)和場景(context)兩個組件來構造一個完整的模型，圖1說明了兩個組件之間的關系，自動機需要引用場景的定義.

在自動機組件中，系統(tǒng)變量在VARIABLES中聲明，其約束在INVATIANTS里定義，并且需要在事件Initialisation中對變量進行初始化賦值.在場景組件中，可以自定義一些數(shù)據(jù)類型如集合，在CONSTANTS聲明一些常量，并且在AXIOMS提出對集合和常量的約束作為公理.

系統(tǒng)的行為是依靠一系列的原子事件EVENTS來實現(xiàn)的，一個事件定義為如下形式:

圖1 Event-B模型組成關系圖Fig.1 Composition relation for Event-B model

其中，lv是事件可能用到的局部變量，g是事件發(fā)生的前條件，R是對變量的賦值操作.Event-B中事件的執(zhí)行必須滿足前提條件g的約束.

1.2 Event-B 常用符號

Event-B的模型描述中經常使用到的一些運算符號，除了基本的交并集合運算外，其他運算如表1所示.

?

1.3 Event-B 驗證機理

自動機和場景中可以定義定理，其中在場景中的形式為T(d，c)，自動機中的形式為T(d，c，v).證明義務確保了提出定理的是可證的.在場景里定義的定理生成如下證明:

在自動機里定理生成的證明形式如下:

為了證明一個描述的正確性，需要保證模型一直保持著不變式I(d，c，v).這里的不變式可以是對變量的類型約束、取值約束，還可以是系統(tǒng)性質.

例如模型中的一個事件ei滿足各種條件約束，則有下式成立:

式中，A是各個公理的合取，I是各不變式的合取，gi是事件ei的前提條件，BAi是事件ei的前后斷言，d表示各集合，c表示各常量，v和v'分別表示事件執(zhí)行前后的變量值.它表述的意義是事件ei執(zhí)行某個操作后，改變了系統(tǒng)變量v的狀態(tài)，狀態(tài)改變后的v'仍要滿足對變量v的約束條件，這是證明的普遍形式，Event-B模型正是靠證明來保證模型的正確性.

2 任務管理需求的形式化模型

嵌入式系統(tǒng)通常是建立在一個嵌入式操作系統(tǒng)內核之上的，由內核提供任務調度和中斷處理操作.任務管理決定了操作系統(tǒng)的實時性能，它涉及到的內容包括任務狀態(tài)遷移，任務控制塊，內核中各種隊列，調度算法等.任務管理實現(xiàn)的核心和基礎是任務狀態(tài)和遷移時序，任務運行狀態(tài)的遷移和任務隊列決定了調度器的實現(xiàn).

SpaceOS2的任務管理要求任務具有7種狀態(tài)，支持64個優(yōu)先級，優(yōu)先級采用靜態(tài)分配.任務調度采用最高優(yōu)先級的搶占式調度策略，同優(yōu)先級任務采用時間片輪轉的方式，可使重要任務盡快得到執(zhí)行，實現(xiàn)快速響應.

2.1 模型對象

本文的建模思想是使用集合與集合之間的關系來描述任務的狀態(tài)變遷，這其中需要用到任務、任務狀態(tài)集、任務狀態(tài)轉換關系、任務變遷時序控制等對象.

對象1.任務，基本的任務控制塊TCB屬性包括狀態(tài)、優(yōu)先級、時間片等.

使用集合Tasks表示任務類型，聲明一個任務t時可以描述為t∈Tasks.任務申請內存空間之后才被加入到任務集合中，為了表示是否已得到申請內存，設置一個函數(shù)isTCB∈Tasks→BOOL，只有映射到TRUE的任務才是被認為分配了內存等資源后創(chuàng)建成功的任務.這些創(chuàng)建成功的任務記為TCBid.

設置任務狀態(tài)集，TaskStatus={executing，ready，delay，block，suspend，suspend_delay，suspend_block};設置任務優(yōu)先級Priority，它是自然數(shù)的一個子集;用任務與各屬性的之間的函數(shù)映射關系來表示TCB屬性，包括狀態(tài)tskStatus，優(yōu)先級tskPrio，延遲時間片個數(shù)delayTicks，剩余時間片個數(shù)leftTicks.其映射關系的約束條件是一個任務只有一個狀態(tài)、優(yōu)先級、延遲時間、剩余時間片，是多對一的函數(shù)映射.

對象4.任務遷移時序，通過設置一些變量標志來作為任務執(zhí)行的時序條件.

createFlag=1表示可以創(chuàng)建任務，創(chuàng)建完成后把標志createFlag置0.當需要觸發(fā)創(chuàng)建任務操作的時候就把標志置為1.其他標志還包括刪除任務標志deleteFlag，延時任務標志delayFlag，恢復任務標志resumeFlag，重啟任務標志restartFlag，調度標志scheduleFlag，任務剩余時間片清零標志clearTickFlag，更新最高優(yōu)先級就緒任務標志updateHPrioFlag.

這些標志的類型都是整數(shù)類型NAT，可以根據(jù)需要賦值為 0，1，2 等.

2.2 模型行為

操作系統(tǒng)對任務管理提出的功能要求包括以下行為操作:創(chuàng)建任務、刪除任務、掛起任務、恢復任務、延時任務、調度任務，通過控制任務的狀態(tài)變遷和對任務集合的操作來實現(xiàn)任務管理.下面以任務調度為例進行介紹.

任務調度需要做的是按照某一調度策略從就緒任務中選擇一個任務運行，將它的狀態(tài)設為運行態(tài).目前的嵌入式實時操作系統(tǒng)通常采用的調度策略是基于優(yōu)先級的搶占式調度與時間片輪轉相結合的調度策略調度操作需要分為3種不同情況:

1)當前任務進行自刪除、延時、阻塞、自掛起等操作時，主動放棄CPU使用權，此時只需從就緒態(tài)任務集中選擇最高優(yōu)先級的任務設為執(zhí)行態(tài)即可.在將當前任務改變狀態(tài)加入相應狀態(tài)集的同時，需要將current狀態(tài)設為none，將scheduleFlag狀態(tài)設為1，此時觸發(fā)以下操作:

2)就緒態(tài)任務集中有新的任務加入，此時觸發(fā)調度.首先選擇最高優(yōu)先級的任務與正在運行的任務進行優(yōu)先級比較，如果就緒任務優(yōu)先級高，則進行切換.當有新任務進入就緒就緒任務集時，就將scheduleFlag狀態(tài)設為2，并將最高優(yōu)先級就緒任務比當前任務優(yōu)先級高作為進行任務切換的一個前提條件，因此有以下操作:

3)二者優(yōu)先級相同，則當前任務與最高優(yōu)先級任務互換，并將最高優(yōu)先級任務的時間片剩余時間設為1.與第二種情況相比需增加一個前提條件:當前任務剩余時間片為0.此外增加了一個操作Clear-Tick，用來表示當前任務執(zhí)行了1個時間片后，剩余執(zhí)行時間清零，開始執(zhí)行下一個同優(yōu)先級就緒任務，因此有以下操作:

在就緒態(tài)任務集狀態(tài)發(fā)生變化時，最高優(yōu)先級任務HPrioTask有可能會發(fā)生改變，此時應及時更新.

3 模型的形式化驗證

Rodin平臺對Event-B產生的證明義務有很好的自動化證明的支持，并且有多種插件幫助證明過程如ProB、SMT求解器等，可以在交互證明時提供幫助.

在不變式中可以加入斷言語句表示系統(tǒng)性質，例如一個任務只能對應一個任務狀態(tài).

這些性質與系統(tǒng)對其他變量的約束一樣，當狀態(tài)發(fā)生改變時，系統(tǒng)會生成相應的證明義務，要求進行驗證.

圖2 ProB對模型的檢驗結果Fig.2 Model checking result by ProB

從圖2可以看到，經過ProB的模型檢驗，任務管理模型沒有發(fā)生死鎖，也沒有不變式違反情況發(fā)生，說明模型是正確的.

之后通過交互式證明器給出顯式的證據(jù)來讓用戶相信系統(tǒng)模型的正確性.這一證明過程在插件SMT的幫助下很方便的證明系統(tǒng)生成的所有證明義務.統(tǒng)計結果如圖3所示.

圖3 證明義務的統(tǒng)計Fig.3 Statistics on proof obliations

利用Rodin平臺上的插件ProB對模型可能存在的死鎖、不變式違反情況等問題應用模型檢驗技術進行了檢測，利用定理證明技術對功能需求涉及到的證明義務及非功能需求的定理性質進行了邏輯推理證明.驗證結果表明任務需求模型不存在死鎖情況，所有事件都有得到運行的機會;模型檢驗沒有發(fā)現(xiàn)不變式違反情況.Event-B模型是依靠變量狀態(tài)改變前后始終保持不變式來保證模型的正確性的.

4 結論

本文對航天嵌入式操作系統(tǒng)SpaceOS2內核的任務管理模塊，應用形式化方法Event-B建立了一個初級模型，該模型描述了內核任務管理的特性，包括任務在不同狀態(tài)之間的變遷、事件執(zhí)行條件約束、任務調度算法等.并利用Rodin平臺提供的交互式定理證明工具驗證來內核形式化模型的正確性.結果表明模型滿足了需求的規(guī)約，在需求階段針對任務管理模塊提出的功能及性質要求是正確的.

［1］WALKER B J，KEMMERER R A，POPEK L.Specification and verification of the UCLA Unix security kernel［J］.Communications of the ACM，1980，23(2):118-131.

［2］BEVIER W.A Verified operating system kernel［D］.Austin:University of Texas，1987.

［3］BIRRELL A D，GUTTAG J V，HORNING J J，et al.Synchronisation primitives for a multiprocessor:a formal specification［J］.ACM SIGOPS Operating Systems Re-view，1987，21(5):94-102

［4］KLEING，ELPHINSTONE K.SeL4:formal verification of an OS kernel［C］//Jeanna Neefe，SOSP'09 Proceedings of the ACM SIGOPS 22ndsymposium on Operating Systems Principles. New York:ACM Press，2009:207-220.

［5］ABRIALJ R.Modeling in Event-B:system and software engineering［M］.Cambridge:Cambridge University Press，2010:12-64.

［6］ABRIALJ R，BUTLER M，HALLERSTEDE S，et al.Rodin:an open toolset for modeling and reasoning in E-vent-B ［J］.International Journal on Software Tools Technology Transfer，2010，12(6):447-466.