周育逵,楊 樺,喬 磊

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

?

基于Event-B的中斷管理需求和設(shè)計(jì)形式化建模與驗(yàn)證方法*

周育逵,楊 樺,喬 磊

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

隨著軟件復(fù)雜度的迅速增長，傳統(tǒng)的基于測試的方法逐漸難以滿足航天器操作系統(tǒng)的可靠性和安全性需求，形式化方法逐漸成為航天器操作系統(tǒng)安全可靠性的有效保障.基于Rodin平臺，采用Event-B形式化語言，通過需求和設(shè)計(jì)重寫、制定精化策略并逐步精化的方法，對航天嵌入式操作系統(tǒng)SpaceOS2的中斷管理模塊建立了需求層和設(shè)計(jì)層形式化模型，將模型檢驗(yàn)和定理證明相結(jié)合，驗(yàn)證模型的正確性并且滿足安全性質(zhì). 關(guān)鍵詞： 中斷管理;形式化驗(yàn)證;Event-B;精化

0 引 言

在航空航天領(lǐng)域，航天器操作系統(tǒng)的安全性因其生命期長，結(jié)構(gòu)復(fù)雜，穩(wěn)定性要求高和出錯(cuò)代價(jià)高昂開始引起了廣泛的關(guān)注.操作系統(tǒng)由于其復(fù)雜性，其正確性很難用定量的方式進(jìn)行描述和說明，由于操作系統(tǒng)軟件在各類航天器計(jì)算機(jī)應(yīng)用中的核心地位，其可靠性至關(guān)重要.隨著軟件復(fù)雜度的迅速增長，傳統(tǒng)的基于測試的方法逐漸難以滿足航天器操作系統(tǒng)的可靠性和安全性需求，形式化方法逐漸成為航天器操作系統(tǒng)安全可靠性的有效保障，采用形式化的方法對操作系統(tǒng)進(jìn)行設(shè)計(jì)和驗(yàn)證[1-2]已經(jīng)得到國際學(xué)術(shù)界的廣泛重視.

形式化方法[3]是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的用以對軟硬件系統(tǒng)進(jìn)行說明、設(shè)計(jì)和驗(yàn)證的語言、技術(shù)和工具的總稱，分為形式化規(guī)約與形式化驗(yàn)證兩個(gè)方面.形式化規(guī)約就是用形式化語言在不同抽象層次上描述系統(tǒng)的行為與性質(zhì).形式化驗(yàn)證是基于已經(jīng)建立的形式化規(guī)約，對軟件的相關(guān)特性進(jìn)行評價(jià)的數(shù)學(xué)分析和證明.形式化驗(yàn)證主要包括模型檢驗(yàn)[4]和定理證明[5]兩個(gè)方面，模型檢驗(yàn)主要是利用對系統(tǒng)問題建立的數(shù)學(xué)模型進(jìn)行自動推理.定理證明一般采用交互式的定理輔助證明器來對系統(tǒng)問題進(jìn)行抽象描述，并以數(shù)學(xué)公式定理的方式表達(dá)系統(tǒng)的功能和性質(zhì)，采用數(shù)學(xué)定理推導(dǎo)演算的方法進(jìn)行驗(yàn)證.

操作系統(tǒng)形式化驗(yàn)證工作可以追溯到20世紀(jì)70年代，美國加利福尼亞大學(xué)洛杉磯分校的Secure Unix項(xiàng)目[6]就對Unix的安全內(nèi)核進(jìn)行了形式化描述與驗(yàn)證工作，其研究重點(diǎn)在于內(nèi)核規(guī)范.美國德克薩斯州大學(xué)的Bevier建立了內(nèi)核形式化模型[7]，Horning[8]對操作系統(tǒng)的規(guī)約進(jìn)行了形式化描述，Zhou和Black[9]運(yùn)用HOL定理證明器對操作系統(tǒng)安全行為操作的形式化描述進(jìn)行了研究.

近年來，國外針對操作系統(tǒng)的驗(yàn)證還有：德國德累斯頓工業(yè)大學(xué)的VFiasco項(xiàng)目[10]、美國霍普金斯大學(xué)的EROS/Coyotos項(xiàng)目[11]、德國的Verisoft項(xiàng)目[12]與后續(xù)的Verisoft-XT項(xiàng)目[13]、澳大利亞國家通訊技術(shù)研究中心的L4.Verified項(xiàng)目[1,14]等.其中，澳大利亞的L4.Verified項(xiàng)目組[1]在2009年宣布成功驗(yàn)證了一個(gè)可以實(shí)際應(yīng)用的操作系統(tǒng)內(nèi)核seL4，并宣布它是第一個(gè)針對功能正確性結(jié)果完全的形式化驗(yàn)證的通用操作系統(tǒng)內(nèi)核.

國內(nèi)研究機(jī)構(gòu)從20世紀(jì)90年代開始進(jìn)行大量的工作，近年來也取得了重要成果，比如中國科學(xué)技術(shù)大學(xué)的μC/OS-Ⅱ驗(yàn)證項(xiàng)目設(shè)計(jì)了并發(fā)精化驗(yàn)證框架并在Coq中實(shí)現(xiàn)了該理論框架[15]，其目標(biāo)是完成嵌入式并發(fā)多任務(wù)操作系統(tǒng)μC/OS-Ⅱ的數(shù)學(xué)驗(yàn)證；南京大學(xué)錢振江博士研究了安全操作系統(tǒng)的形式化設(shè)計(jì)與驗(yàn)證方法[16]，提出了操作系統(tǒng)對象語義模型，并給出如何驗(yàn)證操作系統(tǒng)在運(yùn)行過程中保持安全策略和屬性的形式化描述方法等.

本文基于Rodin[17]平臺，采用Event-B[18]形式化語言，通過需求和設(shè)計(jì)重寫、制定精化策略并逐步精化的方法，對航天嵌入式操作系統(tǒng)SpaceOS2的中斷管理模塊的需求和設(shè)計(jì)進(jìn)行形式化建模，將模型檢驗(yàn)和定理證明相結(jié)合，對模型和安全性質(zhì)進(jìn)行了驗(yàn)證.

1 需求重寫和設(shè)計(jì)重寫

Abrial[18]提到的形式化開發(fā)方法中指出，為了建立正確的系統(tǒng)，首先需要謹(jǐn)慎地編寫需求文檔，進(jìn)行需求重寫，其原因是企業(yè)通用的需求文檔往往晦澀難懂，不適合形式化建模.

本文將需求重寫延伸至設(shè)計(jì)層，把需求重寫和設(shè)計(jì)重寫作為形式化驗(yàn)證的第一步.將原始的需求和設(shè)計(jì)按照以下3類進(jìn)行重新分類整理：

FUN：功能，用于描述系統(tǒng)主要功能，軟件需要完成的具體任務(wù).

ENV：環(huán)境，考慮系統(tǒng)或軟件所處環(huán)境，包括與其相關(guān)的設(shè)備、物理現(xiàn)象、其它軟件/系統(tǒng)/模塊以及用戶.

SAF：安全性質(zhì)，指的是系統(tǒng)需要滿足的一些性質(zhì)，它們能保證系統(tǒng)或軟件正常運(yùn)行，不發(fā)生錯(cuò)誤，不發(fā)生典型的缺陷.

然后對重新整理后的需求項(xiàng)和設(shè)計(jì)項(xiàng)進(jìn)行標(biāo)號，建立精化策略，通過制定精化策略在精化模型中引入需求項(xiàng)和設(shè)計(jì)項(xiàng)并逐步精化，直到完成形式化建模與驗(yàn)證.

2 需求層建模與驗(yàn)證

2.1 需求重寫

對需求規(guī)格說明書中的中斷管理模塊的需求進(jìn)行重寫，按照功能、環(huán)境和安全性質(zhì)進(jìn)行分類標(biāo)號，標(biāo)號以R(Requirement)開頭，并建立中斷管理模塊的原始需求規(guī)格說明和重寫后的需求的對應(yīng)關(guān)系便于追溯.

中斷管理模塊通過中斷管理程序?qū)崿F(xiàn)，對中斷管理模塊相應(yīng)的需求進(jìn)行重寫后共形成功能需求3條，環(huán)境需求2條，安全性質(zhì)1條，如表1所示，并建立原始文檔中的需求和重寫后需求項(xiàng)的對應(yīng)關(guān)系，來說明重寫后的需求能覆蓋原始文檔中的需求.

2.2 需求層精化策略

需求層對中斷管理程序的3個(gè)主要功能建立抽象模型，對外部環(huán)境建立抽象模型，并建立中斷管理和外部環(huán)境之間的交互關(guān)系.

需求層分兩層進(jìn)行精化，在L0-R0層引入功能和環(huán)境需求，在L0-R1層引入安全性質(zhì).精化策略表如表2所示.

表1 功能需求、環(huán)境需求和安全性質(zhì)Tab.1 Requirements of function、environment and safety

表2 需求層精化策略Tab.2 Refinement strategy table of requirement model

注.*表示該項(xiàng)在該層沒有被完全引入

2.3 需求層模型

根據(jù)需求重寫項(xiàng)和需求層精化策略在Event-B內(nèi)建立需求層模型，需求層模型分為L0-R0和L0-R1共2層，由1個(gè)場景(Context)和2個(gè)機(jī)器(Machine)組成，如圖1(a)所示，其中macL0R1是對macL0R0的精化，需求層模型中的機(jī)器和場景間的關(guān)系如圖1(b)所示.

場景ctx0中使用集合、常量和公理定義了模型的靜態(tài)元素，機(jī)器macL0R0和macL0R1分別對應(yīng)需求層的L0-R0層和L0-R1層，機(jī)器定義了模型的動態(tài)行為，包括系統(tǒng)變量(Variables)、不變式(Invariants)、事件(Events).不變式是一個(gè)正確性斷言，它斷言了程序或模型中變量之間的某些聯(lián)系，當(dāng)變量的狀態(tài)發(fā)生改變時(shí)要求改變之后的變量仍然滿足該約束條件，上下文保護(hù)和恢復(fù)、執(zhí)行ISR等操作通過事件進(jìn)行建模.

L0-R0層模型中建立了場景ctx0和機(jī)器macL0R0，描述中斷管理的3個(gè)基本步驟：上下文保護(hù)、執(zhí)行ISR和上下文恢復(fù)，引入和中斷處理程序進(jìn)行交互的外部環(huán)境：中斷源、中斷控制器和IU單元.

在macL0R0中定義了10個(gè)事件：設(shè)置模型狀態(tài)(SetState)、設(shè)置起點(diǎn)(SetBegin)、設(shè)置起點(diǎn)狀態(tài)具體值(BeginWith)、中斷源(IntSrc)、中斷控制器(IntCtrl)、IU單元(IUnit)、上下文保護(hù)(CtxSave)、執(zhí)行ISR(RunISR)、上下文恢復(fù)(CtxRecov)、中斷返回(Return).事件舉例：事件CtxRecov對上下文恢復(fù)進(jìn)行建模，當(dāng)狀態(tài)為ctxRecov時(shí)進(jìn)行上下文恢復(fù)，該條件由衛(wèi)兵grd1進(jìn)行約束，需求層模型中使用布爾賦值將上下文恢復(fù)的操作抽象成act1，在設(shè)計(jì)層精化中進(jìn)行進(jìn)一步精化，CtxRecov的定義如下：

WHEN

grd1: state = ctxRecov

THEN

act1: ctxrecov :∈ BOOL

END

L0-R1層模型中引用了場景ctx0，建立了機(jī)器macL0R1，進(jìn)行的主要操作是對事件間的交互關(guān)系進(jìn)行精化和規(guī)約，從而保證需求層能夠滿足安全性質(zhì).

關(guān)于需求層的安全性質(zhì)，安全性質(zhì)R-SAF-1描述了中斷管理程序的3個(gè)步驟之間的順序關(guān)系，要保證上下文保護(hù)、執(zhí)行ISR、上行文恢復(fù)順序執(zhí)行，根據(jù)已經(jīng)建立的模型，給定狀態(tài)下只有對應(yīng)該狀態(tài)的事件能夠執(zhí)行，即只有在狀態(tài)ctxSave時(shí)才能進(jìn)行上行文保護(hù)，只有在狀態(tài)runISR時(shí)才能執(zhí)行ISR，只有在狀態(tài)ctxRecov時(shí)才能進(jìn)行上行文恢復(fù)，然后由事件TopSequenceCtrl控制狀態(tài)轉(zhuǎn)換，因此該安全性質(zhì)通過在事件TopSequenceCtrl中加入以下衛(wèi)兵進(jìn)行規(guī)約：

grd_save_isr: state = ctxSave ? next_state = runISR

grd_isr_recov: state = runISR ? next_state = ctxRecov

grd_recov_rtn: state = ctxRecov ? next_state = return

精化完成后，需求層模型結(jié)構(gòu)如圖2所示.

2.4 需求層驗(yàn)證

在需求層建模過程中會生成證明義務(wù)(Proof Obligations, PO)，包括建立安全性質(zhì)時(shí)也會生成相應(yīng)的證明義務(wù)，需求層模型的正確性和安全性由以下兩點(diǎn)確保:一是證明義務(wù)能夠被證明，二是模型不存在死鎖和不變式違反案例.

需求層模型中生成的證明義務(wù)都能夠被自動證明，統(tǒng)計(jì)結(jié)果如圖3所示.

使用ProB[19]對macL0R1進(jìn)行模型檢驗(yàn)，沒有死鎖和不變式違反情形，即deadlocked、invariant_violated和invariant_not_checked的計(jì)數(shù)都為0，結(jié)果如圖4所示.

以上驗(yàn)證結(jié)果驗(yàn)證了中斷管理需求層模型的正確性和一致性.中斷管理需求層原始文檔中自然語言需求有15個(gè)，對應(yīng)需求重寫后的功能需求3個(gè)、環(huán)境需求2個(gè)、安全性質(zhì)1個(gè)，通過形式化描述，這些需求和性質(zhì)都被引入到形式化模型中，并生成了21條證明義務(wù)，通過工具驗(yàn)證，模型中所有的證明義務(wù)都得到了證明，并且沒有發(fā)現(xiàn)死鎖和不變式違反案例，從而證明了模型的正確性和安全性.

3 設(shè)計(jì)層建模與驗(yàn)證

3.1 設(shè)計(jì)重寫

對詳細(xì)設(shè)計(jì)中的中斷管理程序的設(shè)計(jì)說明進(jìn)行重寫，按照功能、環(huán)境和安全性質(zhì)進(jìn)行分類標(biāo)號，標(biāo)號以D(Design)開頭.對中斷管理程序的設(shè)計(jì)說明中的流程圖的每個(gè)處理步驟進(jìn)行編號，然后與設(shè)計(jì)重寫后的項(xiàng)目建立對應(yīng)關(guān)系，來說明重寫后的設(shè)計(jì)項(xiàng)能覆蓋原始設(shè)計(jì)項(xiàng)，并建立設(shè)計(jì)重寫后的項(xiàng)目與需求重寫后的項(xiàng)目的對應(yīng)關(guān)系，來說明兩者的一致性.

設(shè)計(jì)重寫后共形成功能項(xiàng)12條，環(huán)境項(xiàng)4條，安全性質(zhì)6條，部分舉例如表3所示.

表3 設(shè)計(jì)層功能、環(huán)境和安全性質(zhì)舉例Tab.3 Part of functions、environments and safeties of design model

3.2 設(shè)計(jì)層精化策略

設(shè)計(jì)層共分4層對需求層建立的抽象模型以及交互關(guān)系進(jìn)行精化.

L1-D0層：L1-D0層對中斷管理的3個(gè)步驟上下文保護(hù)和恢復(fù)、執(zhí)行ISR進(jìn)行精化.一些必須但復(fù)雜的功能在后續(xù)精化層中引入，比如在L1-D0層不引入上下文保護(hù)的判斷條件，在后續(xù)的精化過程中引入判斷條件后再根據(jù)判斷條件將上下文保護(hù)精化成多個(gè)事件.

此外，對外部環(huán)境進(jìn)行適當(dāng)精化，中斷源進(jìn)行中斷請求，中斷控制器進(jìn)行篩選判優(yōu)，IU單元響應(yīng)中斷、設(shè)置PC值，中斷返回恢復(fù)PC值，對初始化操作進(jìn)行精化.

L1-D1層：引入中斷嵌套、開/關(guān)中斷，并根據(jù)嵌套數(shù)、被中斷的程序類型(是否為任務(wù))對上下文保護(hù)和恢復(fù)進(jìn)行分類.

引入一個(gè)事件對嵌套數(shù)計(jì)數(shù).引入中斷屏蔽，并據(jù)此加強(qiáng)中斷響應(yīng)的衛(wèi)兵條件(必須是開中斷并且未被屏蔽)等.考慮上下文保護(hù)和恢復(fù)的精化：引入兩個(gè)事件對上下文保護(hù)進(jìn)行精化，引入兩個(gè)事件對上下文恢復(fù)進(jìn)行精化，引入兩個(gè)事件分別對任務(wù)重調(diào)度和任務(wù)切換進(jìn)行建模.

引入了開關(guān)中斷，因此在IU單元的操作中加入關(guān)中斷操作，中斷返回操作中加入開中斷操作.

L1-D2層：引入窗口上下溢標(biāo)志并根據(jù)標(biāo)志對窗口上下溢的處理，用兩個(gè)事件分別對窗口上溢和下溢進(jìn)行建模.

IU單元和中斷返回中涉及窗口的操作，進(jìn)行相應(yīng)的精化.

L1-D3層：引入各個(gè)事件間的執(zhí)行順序等關(guān)系，描述安全性質(zhì).

設(shè)計(jì)層精化策略表如表4所示.

表4 設(shè)計(jì)層精化策略Tab.4 Refinement strategy table of design model

注：*表示該項(xiàng)在該層沒有被完全引入

3.3 設(shè)計(jì)層模型

根據(jù)設(shè)計(jì)重寫項(xiàng)和設(shè)計(jì)層精化策略在Event-B內(nèi)建立設(shè)計(jì)層模型，設(shè)計(jì)層模型分為L1-D0、L1-D1、L1-D2和L1-D3共4層，建立3個(gè)場景ctx1、ctx2和ctx3，依次對ctx0、ctx1、ctx2進(jìn)行擴(kuò)展(Extend)，建立4個(gè)機(jī)器macL1D0、macL1D1、macL1D2和macL1D3，依次對macL0R1、macL1D0、macL1D1和macL1D2進(jìn)行精化，如圖5(a)所示，設(shè)計(jì)層模型中的機(jī)器和場景間的關(guān)系如圖5(b)所示.

模型精化舉例：L1-D1層引入中斷嵌套后，事件CtxRecov1和TaskReschedule共同精化抽象事件CtxRecov，當(dāng)滿足衛(wèi)兵條件IntNestCnt > 1 ∨ TaskCur = 0時(shí)，由CtxRecov1進(jìn)行有嵌套(嵌套數(shù)>1)或當(dāng)前任務(wù)為0(被中斷的程序不是任務(wù))時(shí)的上下文恢復(fù)，當(dāng)滿足衛(wèi)兵條件IntNestCnt = 1 ∧ TaskCur ≠ 0時(shí)，無嵌套(嵌套數(shù)=1)且當(dāng)前任務(wù)非0(被中斷的程序是任務(wù))，需要調(diào)用任務(wù)重調(diào)度函數(shù)，由TaskReschedule進(jìn)行處理，在TaskReschedule中對need_task_switch進(jìn)行賦值，標(biāo)志后續(xù)是否需要任務(wù)切換.TaskReschedule的定義如下：

REFINES

CtxRecov

WHEN

grd1: state = ctxRecov ∧ setTopSeq = TRUE

grd2: IntNestCnt = 1 ∧ TaskCur ≠ 0

THEN

act1: ctxrecov := TRUE

act2: setTopSeq := FALSE

act3: need_task_switch :∈ BOOL

END

事件CtxRecov1和TaskReschedule共同規(guī)約了功能項(xiàng)D-FUN-9.

下面描述如何對子步驟間的交互關(guān)系進(jìn)行精化.以上下文保護(hù)為例，由事件SetSaveSequence來控制上下文保護(hù)中的各個(gè)子步驟間的狀態(tài)轉(zhuǎn)換，上下文保護(hù)一共分為5個(gè)子步驟，5個(gè)子步驟間是順序執(zhí)行關(guān)系，通過以下衛(wèi)兵條件進(jìn)行規(guī)約：

grd_save_0_1: save_state = save_s0 ? next_save_state = save_s1

grd_save_1_2: save_state = save_s1 ? next_save_state = save_s2

grd_save_2_3: save_state = save_s2 ? next_save_state = save_s3

grd_save_3_4: save_state = save_s3 ? next_save_state = save_s4

執(zhí)行ISR的子步驟間的交互關(guān)系由事件SetIsrSequence控制，上下文恢復(fù)的子步驟間的交互關(guān)系由事件SetRecovSequence和SetSchedSequence共同控制，規(guī)約和精化方法與上文描述的方法一致，不再贅述.

子步驟間交互關(guān)系的精化主要體現(xiàn)在上下文保護(hù)、執(zhí)行ISR和上下文恢復(fù)中，IU單元處理完成后進(jìn)入上下文保護(hù)，當(dāng)處于上下文保護(hù)步驟中時(shí)(inSave = TRUE)，由SetSaveSequence控制上下文保護(hù)中的各個(gè)子步驟間的執(zhí)行順序，當(dāng)跳出上下文保護(hù)步驟時(shí)(┑(inSave = TRUE))，由TopSequenceCtrl控制進(jìn)入下一步驟即執(zhí)行ISR；當(dāng)處于執(zhí)行ISR步驟中時(shí)(inIsr = TRUE)，由SetIsrSequence控制執(zhí)行ISR中的各個(gè)子步驟間的執(zhí)行順序，當(dāng)跳出執(zhí)行ISR步驟時(shí)(┑(inIsr = TRUE))，由TopSequenceCtrl控制進(jìn)入下一步驟即上下文恢復(fù)；當(dāng)處于上下文恢復(fù)步驟中時(shí)(inRecov = TRUE)，由SetRecovSequence控制上下文恢復(fù)中的各個(gè)子步驟間的執(zhí)行順序，當(dāng)跳出上下文恢復(fù)步驟時(shí)(┑(inRecov = TRUE))，由TopSequenceCtrl控制進(jìn)入下一步驟即中斷返回.

下面介紹安全性質(zhì).在L1-D3層模型中對設(shè)計(jì)層的安全性質(zhì)進(jìn)行規(guī)約，比如D-SAF-5對應(yīng)不變式inv_DSAF5_1和inv_DSAF5_2，其中inv_DSAF5_1的含義是關(guān)中斷時(shí)不能進(jìn)行中斷響應(yīng)，具體內(nèi)容如表5所示.

表5 設(shè)計(jì)層安全性質(zhì)的規(guī)約Tab.5 Specifications for safeties of design model

精化完成后，設(shè)計(jì)層模型結(jié)構(gòu)如圖6所示.

3.4 設(shè)計(jì)層驗(yàn)證

在設(shè)計(jì)層建模過程中會生成證明義務(wù)，包括建立安全性質(zhì)時(shí)也會生成相應(yīng)的證明義務(wù)，設(shè)計(jì)層模型中生成的證明義務(wù)都能夠被證明，統(tǒng)計(jì)結(jié)果如圖7 所示.

使用ProB對macL1D3進(jìn)行模型檢驗(yàn)，沒有死鎖和不變式違反情形，即deadlocked、invariant_violated和invariant_not_checked的計(jì)數(shù)都為0，結(jié)果如圖8所示.

以上驗(yàn)證結(jié)果驗(yàn)證了中斷管理設(shè)計(jì)層的正確性和一致性.中斷管理設(shè)計(jì)層原始文檔中的項(xiàng)目有50個(gè)，對應(yīng)設(shè)計(jì)重寫后的功能項(xiàng)12個(gè)，并針對設(shè)計(jì)層列出環(huán)境項(xiàng)目4個(gè)、安全性質(zhì)6個(gè)，通過形式化描述，這些功能項(xiàng)和環(huán)境項(xiàng)都被引入到形式化模型中，并在模型中建立了安全性質(zhì)的形式化描述，共成了177條(198減掉需求層21條)證明義務(wù)，通過工具驗(yàn)證，模型中所有的證明義務(wù)都得到了證明，并且沒有發(fā)現(xiàn)死鎖和不變式違反案例，從而證明了模型的正確性和安全性.

4 設(shè)計(jì)層和需求層的一致性

通過設(shè)計(jì)重寫后的項(xiàng)目與需求重寫后的項(xiàng)目的對應(yīng)關(guān)系可知，設(shè)計(jì)重寫項(xiàng)和需求重寫項(xiàng)能夠一一對應(yīng)，這保證了重寫后設(shè)計(jì)和需求的一致性.在Rodin平臺下，設(shè)計(jì)層第0層模型macL1D0直接由需求層最后一層模型macL0R1通過Event-B的refine機(jī)制建立，并且模型macL1D0生成的證明義務(wù)都得到證明，而且不存在不變式違反情形，從而保證了Event-B模型中設(shè)計(jì)層和需求層的一致性.原始需求和設(shè)計(jì)文檔、需求和設(shè)計(jì)重寫文檔以及Event-B模型間的一致性關(guān)系如圖9所示.

5 結(jié) 論

本文基于Rodin平臺，采用Event-B形式化語言，通過需求和設(shè)計(jì)重寫、制定精化策略并逐步精化的方法，對航天嵌入式操作系統(tǒng)SpaceOS2的中斷管理模塊建立了需求層和設(shè)計(jì)層形式化模型，將模型檢驗(yàn)和定理證明相結(jié)合，驗(yàn)證了模型的正確性并且滿足安全性質(zhì)，并且驗(yàn)證了設(shè)計(jì)模型和需求模型的一致性.

[1] KLEIN G, ELPHINSTONE K, HEISER G, et al. SeL4: formal verification of an OS kernel[J]. ACM Symposium on Operating Systems Principles, 2009:207-220.

[2] KLEIN G, ANDRONICK J, ELPHINSTONE K, et al. comprehensive formal verification of an os microkernel[J]. ACM Transactions on Computer Systems, 2014, 32(1):136-156.

[3] WOODCOCK J, LARSEN P G, BICARREGUI J, et al. Formal methods: practice and experience[J]. ACM Computing Surveys, 2009, 41(4):1729-1739.

[4] CLARKE E M, GRUMBERG O, PELED D. Model checking[M]. MIT press, 1999.

[5] HOARE C A R, JIFENG H. Unifying theories of programming[M]. Englewood Cliffs: Prentice Hall, 1998.

[6] WALKER B J, KEMMERER R A, POPEK G J. Specification and verification of the ucla unix security kernel[J]. Communications of the ACM, 1980, 23(2):118-131.

[7] BEVIER W R. A verified operating system kernel[M].The University of Texas at Austin. 1987.

[8] BIRRELL A D, GUTTAG J V, HORNING J J, et al. Synchronisation primitives for a multiprocessor: a formal specification[C]//The 11thACM Symposium on Operating Systems Principles. ACM, 1987:94-102.

[9] ZHOU D, BLACK P E. Formal specification of operating system operations[C]// Process. IEEE TC-ECBS Working Group WG10.1. New York: IEEE, 2001:69-73.

[10] HOHMUTH M, TEWS H. The VFiasco approach for a verified operating system[J]. Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, 2005

[11] SHAPIRO J, DOERRIE M S, NORTHUP E, et al. Towards a verified, general-purpose operating system kernel[C]//FM Workshop on OS Verification. Technical Report 0401005T-1, National ICT Australia. 2004:1-19.

[12] DAUM M, SCHIRMER N W, SCHMIDT M. Implementation correctness of a real-time operating system[C]//Software Engineering and Formal Methods, the 7thIEEE International Conference on Software Engineering and Formal Methods. New York: IEEE, 2009:23-32.

[13] BAUMANN C, BORMER T. Verifying the pikeos microkernel: first results in the verisoft xt avionics project[C]//Doctoral Symposium on Systems Software Verification (DS SSV’09) Real Software, Real Problems, Real Solutions. 2009:20-22.

[14] ELPHINSTONE K, HEISER G. From L3 to seL4 what have we learnt in 20 years of L4 microkernels?[J]. ACM Sigops Symposium on Operating Systems Principles, 2013:133-150.

[15] LIANG H, FENG X, FU M. Rely-guarantee-based simulation for compositional verification of concurrent program transformations[J]. ACM Transactions on Programming Languages & Systems, 2014, 36(1):307-323.

[16] 錢振江. 安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D]. 南京: 南京大學(xué), 2013. QIAN Z J. Research on methodology of formal design and verification for security operating system[D]. Nanjing: Nanjing University, 2013.

[17] JASTRAM M, BUTLER P M. Rodin user’s handbook: covers rodin v.2.8[M]. CreateSpace Independent Publishing Platform, 2014.

[18] ABRIAL J R. Modeling in Event-B: system and software engineering[M]. Cambridge University Press, 2010.

[19] LEUSCHEL M, BUTLER M. ProB: An automated analysis toolset for the B method[J]. International Journal on Software Tools for Technology Transfer, 2008, 10(2):185-203.

Formal Modeling and Verification Method of Interrupt-ManagementRequirement and Design Based on Event-B

ZHOU Yukui, YANG Hua, QIAO Lei

(BeijingInstituteofControlEngineering,Beijing100190，China)

With the rapid growth of software complexity, the traditional testing method is gradually difficult to meet the reliability and security requirements of spacecraft operating system. Formal method is gradually becoming an effective guarantee for spacecraft operating system security and reliability. Based on the Rodin platform, using Event-B formal language, through the requirements and design rewrite and formulate the refinement strategy and stepwise refinement method, the requirement layer and design layer formal model is established for the interrupt-management module of the embedded operating system SpaceOS2. Model checking and theorem proving are combined to verify the validity and safety of the model.

interrupt-management; formal verification; Event-B; refinement

*國家自然科學(xué)基金資助項(xiàng)目(61632005, 61502031).

2017-03-07

周育逵(1989—)，男，碩士研究生，研究方向?yàn)榍度胧讲僮飨到y(tǒng)、形式化方法；楊 樺(1969—)，女，研究員，研究方向?yàn)楦呖尚挪僮飨到y(tǒng)、星載容錯(cuò)計(jì)算機(jī)；喬 磊(1982—)，男，高級工程師，研究方向?yàn)椴僮飨到y(tǒng)模型設(shè)計(jì)、存儲管理、文件系統(tǒng).

TP311

A

1674-1579(2017)03-0071-08

10.3969/j.issn.1674-1579.2017.03.012