張錦坤，楊孟飛，喬 磊,3，楊 樺，劉 波

0 引 言

隨著航天事業(yè)的迅猛發(fā)展，空間任務(wù)的規(guī)模及復(fù)雜度上升，空間飛行器上的軟件規(guī)模也隨之增加.操作系統(tǒng)作為計算機(jī)系統(tǒng)中硬件和軟件資源的管理者，其可靠性和和安全性也越發(fā)重要.操作系統(tǒng)中的任何一個微小的錯誤都可能導(dǎo)致整個系統(tǒng)的崩潰，因此操作系統(tǒng)應(yīng)該是一個高可靠、高可信的軟件系統(tǒng)，這是保證所有應(yīng)用軟件能可靠運行的基礎(chǔ).形式化方法[1]逐漸成為航天器操作系統(tǒng)可信性的有效保障，采用形式化的方法對操作系統(tǒng)進(jìn)行設(shè)計和驗證[2-5]已經(jīng)得到國際學(xué)術(shù)界的廣泛重視.

國內(nèi)外對操作系統(tǒng)的形式化驗證開展了一些研究，澳大利亞的NICTA實驗室對操作系統(tǒng)內(nèi)核L4開展了形式化驗證工作，并發(fā)布了新一代嵌入式操作系統(tǒng)seL4[6-7]；耶魯大學(xué)的邵中將自動化定理證明的優(yōu)點與基于VeriML/OCAP的認(rèn)證編程框架的模塊化表達(dá)相結(jié)合[8]，對可驗證的安全內(nèi)核做了一定的研究；馮新宇等人開發(fā)了一個驗證操作系統(tǒng)的框架[9-10]，提出了對內(nèi)核建模和全局性質(zhì)驗證的方法；NELSON等人介紹了一種關(guān)于OS內(nèi)核的設(shè)計、實現(xiàn)和形式化驗證的方法[11]，用Z3 SMT solver檢驗了50個系統(tǒng)調(diào)用和陷阱處理；WEN SU和JEAN-RAYMOND ABRIAL等人用Event-B方法形式化開發(fā)了一個實時系統(tǒng)的內(nèi)存管理模塊[12-13]；錢振江等人對安全操作系統(tǒng)的形式化驗證做了相關(guān)研究[14-18]，采用操作系統(tǒng)對象語義模型(OSOSM)對系統(tǒng)的設(shè)計進(jìn)行形式化建模；北京控制工程研究所也對操作系統(tǒng)的形式化驗證做了一定的研究[19-22]，用Event-B方法對操作系統(tǒng)的一些模塊進(jìn)行了形式化建模和驗證.不過當(dāng)前對操作系統(tǒng)形式化驗證的研究工作要么是針對單個模塊，要么是從代碼反推需求規(guī)約，自上而下的從需求到設(shè)計再到實現(xiàn)層的完整的形式化驗證還比較少.需求層的形式化驗證是操作系統(tǒng)形式化驗證的一部分，能夠更早地發(fā)現(xiàn)是否有潛在的錯誤，有助于完成整個操作系統(tǒng)的形式化驗證，確保整個操作系統(tǒng)的安全性和可靠性.

航天器計算機(jī)系統(tǒng)一般采用中斷驅(qū)動型多任務(wù)并發(fā)嵌入式操作系統(tǒng)，其系統(tǒng)結(jié)構(gòu)復(fù)雜，具有多任務(wù)并發(fā)、中斷頻發(fā)且嵌套、時序固定等特性.圖1示例了一個典型系統(tǒng)，包括6個任務(wù)(4個固定任務(wù)，2個隨機(jī)任務(wù))，4個中斷(2個周期性中斷，2個隨機(jī)中斷).4個任務(wù)都必須在固定時間點啟動，所有任務(wù)必須在規(guī)定時間期限內(nèi)完成.針對這類軟件的主要驗證技術(shù)包括測試技術(shù)和形式化技術(shù).測試是目前保證可靠性而廣泛使用的技術(shù)，但系統(tǒng)運行的狀態(tài)空間大，測試能發(fā)現(xiàn)問題，但不能說明沒有問題，無法從根本上保障操作系統(tǒng)的可靠性.而形式化驗證是使用邏輯推理系統(tǒng)來保證計算機(jī)程序正確性的方法之一.通過形式化的程序邏輯來驗證程序是否滿足給定規(guī)范，并通過顯式的證明來使用戶確信驗證結(jié)果的正確性，是保證軟件可信性的有效方法之一，將成為更加有效實現(xiàn)“零缺陷”的技術(shù).

圖1 中斷驅(qū)動型多任務(wù)并發(fā)操作系統(tǒng)Fig.1 Interrupt-driven multitasking concurrent operating system

本文在分析某典型航天器操作系統(tǒng)SpaceOS2需求的基礎(chǔ)上,利用有限狀態(tài)機(jī)方法進(jìn)行形式化建模，給出全局性質(zhì)的形式化定義，并在Coq中進(jìn)行了形式化驗證.證明顯示SpaceOS2在需求層滿足提出的全局性質(zhì).

1 系統(tǒng)需求

操作系統(tǒng)的需求是硬件加電后能夠執(zhí)行調(diào)度器軟件，在規(guī)定的資源和時間要求下調(diào)度器對任務(wù)進(jìn)行調(diào)度執(zhí)行，并且能夠響應(yīng)中斷.在整個運行過程中，操作系統(tǒng)還應(yīng)該滿足一些全局性質(zhì)，確保任務(wù)的安全順利執(zhí)行.

1.1 系統(tǒng)組成

操作系統(tǒng)根據(jù)系統(tǒng)功能可以劃分為7個部分，初始化、任務(wù)管理、中斷管理、時間管理、內(nèi)存管理、任務(wù)間通信管理和外設(shè)管理，如表1所示.

表1 不同組成部分及其功能Tab.1 Different components and their functions

其中任務(wù)管理、中斷管理和時間管理這3個模塊構(gòu)成了最小系統(tǒng)，可以反映操作系統(tǒng)最基本的行為特征，針對安全關(guān)鍵系統(tǒng)的操作系統(tǒng)模式可以完全覆蓋，這樣既簡化了系統(tǒng)模型，又涵蓋了所有核心要素，便于建模與驗證.

1.2 任務(wù)狀態(tài)

任務(wù)狀態(tài)反映任務(wù)執(zhí)行過程的變化，這些狀態(tài)隨著任務(wù)的執(zhí)行和外部條件的變化而轉(zhuǎn)換.操作系統(tǒng)中，任務(wù)狀態(tài)一般包含以下5種：就緒態(tài)、阻塞態(tài)、掛起態(tài)、睡眠態(tài)和運行態(tài).本文針對典型的航天器操作系統(tǒng)工程應(yīng)用，其任務(wù)狀態(tài)包括就緒態(tài)、運行態(tài)和掛起態(tài)三個核心狀態(tài).

(1)就緒態(tài)(Ready)：處于此狀態(tài)的任務(wù)除了等待CPU外，不需要等待其他資源；

(2)阻塞態(tài)(Pend)：由于一些資源不可用而阻塞的狀態(tài)(等待信號量、消息)；

(3)掛起態(tài)(Suspend)：任務(wù)進(jìn)行了掛起操作的狀態(tài).

圖2 任務(wù)狀態(tài)轉(zhuǎn)移Fig.2 Task state transition

1.3 系統(tǒng)狀態(tài)

隨著任務(wù)的執(zhí)行和外部條件的變化，操作系統(tǒng)狀態(tài)也在發(fā)生著變化.系統(tǒng)狀態(tài)包括兩部分，一是任務(wù)列表，也就是各個任務(wù)的狀態(tài)；二是其他外部條件的狀態(tài)，比如中斷開或關(guān).根據(jù)不同時刻任務(wù)狀態(tài)的不同，系統(tǒng)狀態(tài)也不盡相同.

1.4 全局性質(zhì)

操作系統(tǒng)應(yīng)該滿足一些全局性質(zhì)，不僅在初始狀態(tài)滿足，并且系統(tǒng)由初始狀態(tài)執(zhí)行動作到達(dá)的任意狀態(tài)依然保持滿足.本文分別從任務(wù)、中斷和時間3方面考慮，提煉出6條核心全局性質(zhì)，即在驗證過程中需要證明的定理：

(1)系統(tǒng)中有且只有一個任務(wù)狀態(tài)為運行態(tài)；

(2)運行任務(wù)掛起放棄CPU后只能進(jìn)入掛起態(tài)；

(3)控制周期中斷和時間片中斷不能同時發(fā)生；

(4)任務(wù)狀態(tài)不能直接從就緒態(tài)轉(zhuǎn)為掛起態(tài)；

(5)只能在任務(wù)啟動點調(diào)度新任務(wù)；

(6)空閑任務(wù)不能在啟動點調(diào)度.

其中任務(wù)啟動點指的是每個應(yīng)用任務(wù)劃分好的固定時間片的啟動時刻，在每個任務(wù)啟動點調(diào)度執(zhí)行對應(yīng)的應(yīng)用任務(wù).

2 有限狀態(tài)機(jī)建模方法

有限狀態(tài)機(jī)[23]是描述有限個系統(tǒng)狀態(tài)以及在這些狀態(tài)之間的轉(zhuǎn)移和動作等行為的數(shù)學(xué)模型，現(xiàn)已被廣泛應(yīng)用于計算機(jī)科學(xué)、軟件工程和自動控制等領(lǐng)域，成為計算機(jī)軟件、硬件和網(wǎng)絡(luò)及控制等系統(tǒng)常見的形式化模型之一.有限狀態(tài)機(jī)可以很好地表達(dá)并發(fā)行為，適合并發(fā)系統(tǒng)的刻畫，能夠精確表現(xiàn)系統(tǒng)狀態(tài)之間的遷移；而且狀態(tài)機(jī)方法易于書寫、驗證，也容易轉(zhuǎn)變成設(shè)計或程序代碼.不過在面臨較大規(guī)模系統(tǒng)的時候，有限狀態(tài)機(jī)建模將會十分繁瑣和復(fù)雜.

在操作系統(tǒng)需求層，可以忽略掉底層的細(xì)節(jié)，舍去復(fù)雜數(shù)據(jù)結(jié)構(gòu)進(jìn)行化簡，從而在頂層抽象出一個有限狀態(tài)機(jī)模型來研究系統(tǒng)運行過程.一個有限狀態(tài)機(jī)可以由一個五元組[24]表示：

M=(Q，∑，q0，F(xiàn)，δ)

其中，Q是系統(tǒng)狀態(tài)的非空有限集合；∑是輸入信息或條件的集合；q0是初始狀態(tài)且q0∈S；δ是狀態(tài)轉(zhuǎn)移函數(shù)，可以表示為δ：Q×∑→Q.在一般的有限狀態(tài)機(jī)模型中，存在一個終止?fàn)顟B(tài)軟件集合F，且F?S，經(jīng)過一段時間的運行后，狀態(tài)機(jī)歷經(jīng)一些狀態(tài)遷移，到達(dá)運行的最后狀態(tài)F.但是操作系統(tǒng)是一個連續(xù)運行的軟件，在啟動之后就永遠(yuǎn)執(zhí)行，有外部終止操作的話恢復(fù)到初始狀態(tài)，不存在終止?fàn)顟B(tài).因此本文采用的狀態(tài)機(jī)由四元組表示：

M=(Q，∑，q0，δ)

2.1 系統(tǒng)狀態(tài)集合

操作系統(tǒng)在運行過程中只能處于某一個已知的確定狀態(tài)，比如在狀態(tài)q0，任務(wù)0(即空閑任務(wù))處于運行態(tài)而其他任務(wù)都處于掛起態(tài)；在qm狀態(tài)時，任務(wù)m處于運行態(tài)而其他任務(wù)都處于掛起態(tài).同時在不同狀態(tài)下，其他外部環(huán)境也有所差異，比如是否允許時間片中斷等.不同時刻的系統(tǒng)狀態(tài)組成了系統(tǒng)狀態(tài)集合.

2.2 輸入條件

操作系統(tǒng)在運行過程中接受某一確定的輸入值，根據(jù)這些輸入值采取不同的動作.這些輸入值包括控制周期中斷、時間片中斷和任務(wù)提前結(jié)束等.

2.3 初始狀態(tài)

操作系統(tǒng)經(jīng)過初始化后，創(chuàng)建了若干任務(wù)，可以執(zhí)行調(diào)度器軟件并響應(yīng)緊急事件.此時系統(tǒng)處于初始狀態(tài)q0：空閑任務(wù)處于運行態(tài)，其他任務(wù)都處于掛起態(tài)；并且系統(tǒng)在等待第一個輸入值.

2.4 狀態(tài)轉(zhuǎn)移函數(shù)

狀態(tài)轉(zhuǎn)移函數(shù)表示操作系統(tǒng)的狀態(tài)轉(zhuǎn)移規(guī)則.某一時刻操作系統(tǒng)處于某一狀態(tài)qn，同時接收到某一輸入值an，則通過函數(shù)δ可以推出下一時刻操作系統(tǒng)的狀態(tài)為qm=(qn,an).按照圖1所示的操作系統(tǒng)，每個任務(wù)劃分好時間片，在固定時間點按周期運行，因此在任一時刻下，每個任務(wù)的狀態(tài)都是確定的，并且中斷狀態(tài)也是確定的，那么按照本文定義，系統(tǒng)狀態(tài)也是確定的，不存在一個事件對應(yīng)多個動作的情況，即狀態(tài)機(jī)是確定有限狀態(tài)機(jī).

3 SpaceOS2建模

SpaceOS2是由北京控制工程研究所研制的第二代航天嵌入式實時操作系統(tǒng)，在多個航天型號任務(wù)上得到了實際應(yīng)用.本文將有限狀態(tài)機(jī)建模方法應(yīng)用于在航天器上廣泛應(yīng)用的SpaceOS2，為系統(tǒng)狀態(tài)機(jī)模型進(jìn)行形式化建模包含兩部分工作：一是描述內(nèi)核狀態(tài)和輸入條件，即狀態(tài)集合和轉(zhuǎn)移條件；二是描述內(nèi)核操作的抽象規(guī)范，即狀態(tài)轉(zhuǎn)移函數(shù).

3.1 內(nèi)核狀態(tài)和輸入條件

(TaskState)state：:=R(ready)|E(running)|S(suspend)

(Tasklist)tasklist：:=nil|state list

(Controlflag)controlflag ::=True|False

(Timesliceflag)timesliceflag：:=True|False

(Systate)systate::={tasklist,controlflag,timesliceflag}

(Time)t∈Nat

(TimeStart) ts∈Nat

(Event)event：:=IntControl (t)| IntTimeslice(t)| TaskEnd(t)

SpaceOS2系統(tǒng)狀態(tài)systate包含3部分：任務(wù)列表tasklist，控制周期中斷響應(yīng)標(biāo)志controlflag和時間片中斷響應(yīng)標(biāo)志timesliceflag.任務(wù)列表tasklist是所有任務(wù)的任務(wù)狀態(tài)列表，每個系統(tǒng)狀態(tài)對應(yīng)一個任務(wù)列表.任務(wù)狀態(tài)有三種類型：就緒態(tài)、運行態(tài)和掛起態(tài).操作系統(tǒng)響應(yīng)的中斷有兩種，控制周期中斷和時間片中斷，根據(jù)是否響應(yīng)某種中斷，標(biāo)志為Ture或者False兩種狀態(tài).事件包含3類：控制周期中斷IntControl、時間片中斷IntTimeslice和任務(wù)提前結(jié)束TaskEnd，并且?guī)в袝r間t，時間t是離散自然數(shù).ts指的是任務(wù)啟動點應(yīng)用于某航天器的SpaceOS2在初始化時創(chuàng)建了12個任務(wù)，依次為10個應(yīng)用任務(wù)，1個空閑任務(wù)和1個系統(tǒng)任務(wù).其中系統(tǒng)任務(wù)總是處于掛起態(tài)，其他11個任務(wù)在不同時刻處于運行態(tài)時，對應(yīng)不同的系統(tǒng)狀態(tài).

初始狀態(tài)下只有空閑任務(wù)處于運行態(tài)，其他任務(wù)處于掛起態(tài)，因此初始任務(wù)列表定義為：init_tasklist::=(S，S，S，S，S，S，S，S，S，S，E，S).并且初始狀態(tài)在等待控制周期中斷到來，不允許時間片中斷，所以初始狀態(tài)s0定義為：

init_state(s0)::={tasklist=init_tasklist,controlflag=True,timesliceflag=False}

控制周期中斷到來之后，時間片中斷開關(guān)打開，其他任務(wù)開始調(diào)度執(zhí)行，任務(wù)n(1≤n≤10)處于運行態(tài)時對應(yīng)的任務(wù)列表tasklist_n中，第n個任務(wù)狀態(tài)為運行態(tài)E，空閑任務(wù)處于就緒態(tài)R，其他任務(wù)處于掛起態(tài).系統(tǒng)狀態(tài)可以定義為：

state_n(sn)::={tasklist=tasklist_n,controlflag=False,timesliceflag = True }

此外當(dāng)應(yīng)用任務(wù)在時間片中斷到來之前提前結(jié)束時，空閑任務(wù)執(zhí)行，其他任務(wù)掛起，此時的任務(wù)列表和初始任務(wù)列表相同，但是當(dāng)前狀態(tài)允許響應(yīng)時間片中斷而不響應(yīng)控制周期中斷，因此這是一個不同于初始狀態(tài)的中間狀態(tài)state_M：

state_M(sm)::={tasklist=init_tasklist,controlflag=False,timesliceflag = True }

至此得到所有的12個系統(tǒng)狀態(tài)，Q={s0，s1，s2，s3，s4，s5，s6，s7，s8，s9，s10，sM}.

3.2 狀態(tài)轉(zhuǎn)移函數(shù)

確定了各個狀態(tài)以及相關(guān)條件后，還要確立各個狀態(tài)之間的轉(zhuǎn)換關(guān)系.操作系統(tǒng)啟動之后進(jìn)行初始化，處于初始狀態(tài)，控制周期中斷到來之后，轉(zhuǎn)移到s1狀態(tài)并開始時間片計數(shù)，允許響應(yīng)時間片中斷.之后每4 ms來一個時間片中斷，如果此時刻是新任務(wù)的啟動點(ts)則轉(zhuǎn)換到下一個狀態(tài)；否則繼續(xù)執(zhí)行當(dāng)前任務(wù).另外如果任務(wù)提前結(jié)束，則切換到空閑任務(wù)執(zhí)行，進(jìn)入sM狀態(tài).40個時間片之后，不再響應(yīng)時間片中斷，回到初始狀態(tài)等待下一個控制周期中斷到來.具體的狀態(tài)轉(zhuǎn)移圖如圖3所示，其中IntControl代表控制周期中斷，TE代表事件任務(wù)提前結(jié)束(TaskEnd)，IT和ITS都是時間片中斷(IntTimeslice)，ITS代表當(dāng)前中斷時刻是新任務(wù)的啟動點.

圖3 狀態(tài)轉(zhuǎn)移圖Fig.3 State transition diagram

結(jié)合狀態(tài)轉(zhuǎn)移圖并進(jìn)行規(guī)約后，給出狀態(tài)轉(zhuǎn)移函數(shù)的定義，涉及到兩個參數(shù)，一個是帶時間的事件類型，另外一個是當(dāng)前的系統(tǒng)狀態(tài).

圖4 狀態(tài)轉(zhuǎn)移函數(shù)Fig.4 State transition function

4 形式化驗證

在采用了有限狀態(tài)機(jī)方法對SpaceOS2進(jìn)行了形式化描述和建模之后，接下來要采用合適的工具對其進(jìn)行形式化驗證.Coq是目前國際上交互式定理證明領(lǐng)域的主流工具，本文選擇定理證明工具Coq來進(jìn)行驗證，首先要對應(yīng)地在Coq中對模型進(jìn)行描述，然后對提煉出的性質(zhì)進(jìn)行形式化定義并且采用恰當(dāng)?shù)淖C明策略進(jìn)行驗證，說明操作系統(tǒng)SpaceOS2在需求層滿足提出的全局性質(zhì).

4.1 內(nèi)核建模

為了驗證操作系統(tǒng)是否滿足提出的全局性質(zhì)，要根據(jù)第3節(jié)建立的有限狀態(tài)機(jī)模型在Coq中相應(yīng)地進(jìn)行描述建模.因為建立的帶時間的事件驅(qū)動任務(wù)轉(zhuǎn)移系統(tǒng)模型，要依次定義時間、轉(zhuǎn)移事件、任務(wù)狀態(tài)和系統(tǒng)狀態(tài)等類型，并且構(gòu)造狀態(tài)轉(zhuǎn)移函數(shù)transfer.涉及到的參數(shù)有帶時間的事件類型和前一個狀態(tài).在3種事件驅(qū)動下，進(jìn)行固定時間點的任務(wù)調(diào)度轉(zhuǎn)移.

4.2 性質(zhì)描述

要驗證系統(tǒng)模型是否滿足全局性質(zhì)，首先要明確證明目標(biāo)，即在Coq環(huán)境下要給出性質(zhì)的定義.形式化描述全局性質(zhì)時，首先將性質(zhì)涉及到的數(shù)據(jù)結(jié)構(gòu)從內(nèi)核狀態(tài)中取出，然后描述這些數(shù)據(jù)結(jié)構(gòu)之間的關(guān)系.在此給出幾條性質(zhì)的形式化描述，在Coq中驗證時根據(jù)此描述進(jìn)行相應(yīng)的擴(kuò)充和類型定義.

性質(zhì)1 有且只有一個任務(wù)狀態(tài)為運行態(tài)

? systate,count (state = running)=1

性質(zhì)2 任務(wù)放棄CPU后只能進(jìn)入掛起態(tài)

? task,state =E∧event =TaskEnd?astate=S

性質(zhì)3 控制周期中斷和時間片中斷不能同時發(fā)生

? systate,and (controlflag,timesliceflag)=False

4.3 證明思路

證明系統(tǒng)滿足一個全局性質(zhì)，就要全方面考慮，不僅要證明系統(tǒng)在初始狀態(tài)滿足性質(zhì)，還要證明從初始狀態(tài)執(zhí)行任意動作到達(dá)的新狀態(tài)也滿足性質(zhì).在本文建立的狀態(tài)機(jī)模型中，就是要證明操作系統(tǒng)在初始化之后的初始狀態(tài)滿足性質(zhì)，并且在每個狀態(tài)之間轉(zhuǎn)換時也要滿足性質(zhì).以性質(zhì)1為例，證明思路如下：

(1)初始狀態(tài) init_state只有一個任務(wù)狀態(tài)為運行態(tài)；

(2)初始狀態(tài)轉(zhuǎn)換到s1狀態(tài)，只有一個任務(wù)狀態(tài)為運行態(tài)；

(3)s1狀態(tài)轉(zhuǎn)換到中間狀態(tài)，只有一個任務(wù)狀態(tài)為運行態(tài)；

(4)s1狀態(tài)轉(zhuǎn)換到s2狀態(tài)，只有一個任務(wù)狀態(tài)為運行態(tài)；

(5)中間狀態(tài)轉(zhuǎn)換到s2狀態(tài)，只有一個任務(wù)狀態(tài)為運行態(tài)；

(6)s1狀態(tài)轉(zhuǎn)換到s1狀態(tài)，只有一個任務(wù)狀態(tài)為運行態(tài).

同理，按照狀態(tài)轉(zhuǎn)移圖的每一個出邊和入邊，證明每一次轉(zhuǎn)換都滿足性質(zhì)1，這樣就能保證建立的操作系統(tǒng)模型滿足該性質(zhì).

4.4 證明策略

明確了證明目標(biāo)和思路之后，要采取恰當(dāng)?shù)淖C明策略，將復(fù)雜的目標(biāo)進(jìn)行逐步簡化和推理，直到證明完成.以驗證初始狀態(tài)滿足性質(zhì)1為例，首先定義了valid_state，即這個狀態(tài)下只有一個任務(wù)處于運行態(tài).相關(guān)證明策略及推演過程如下所示.橫線之上代表此時的條件，橫線下方代表此時待證明的目標(biāo).其他5條性質(zhì)的證明與性質(zhì)1的證明類似.

(1)intros

通過這條證明策略，將所有條件引入證明環(huán)境，明確證明目標(biāo).此時出現(xiàn)了一個新的條件H，說明init_state的具體構(gòu)造.現(xiàn)在的證明目標(biāo)依舊是說明初始狀態(tài)為valid_state.

1subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

valid_stateinit_state

(2)rewrite H

重寫條件H，用等號右邊項代替左邊項，替換證明目標(biāo)里的init_state，進(jìn)一步將證明目標(biāo)明確.

1subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

valid_state{|TL：=init_tasklist；CF：=True；TF：=False|}

(3)unfold valid_state

要證明初始狀態(tài)為有效狀態(tài)，首先將有效狀態(tài)的定義展開，即按照之前在形式化描述時統(tǒng)計任務(wù)狀態(tài)為運行態(tài)的任務(wù)個數(shù)，證明運行態(tài)的任務(wù)只有一個.

1subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

count_occtaskstate_dec(TL{|TL：=init_tasklist；CF：=True；TF：=False|})Running=1

(4)simpl

進(jìn)行化簡，將庫函數(shù)count_occ展開，逐個比對當(dāng)前任務(wù)列表里每一個任務(wù)狀態(tài)，累計任務(wù)狀態(tài)為運行態(tài)的任務(wù)個數(shù).

(5)destruct (taskstate_dec Suspend Running)

分情況討論，比較Suspend和Running兩個狀態(tài)，此時引入了一個新的條件e，同時證明目標(biāo)被分解為兩個子目標(biāo)，要依次驗證這兩個子目標(biāo).

2subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

e：Suspend=Running

S(S(S(S(S(S(S(S(S(S(iftaskstate_decRunningRunningthen2else1))))))))))=1

(iftaskstate_decRunningRunningthen1else0)=1

(6)inversion e

證明第一個子目標(biāo)時，因為Suspend明顯不等于Running，因此翻轉(zhuǎn)條件e，消除掉子目標(biāo)1.此時出現(xiàn)一個新的條件n.

1subgoal

init_state：Rdata

H：init_state={ |TL：=init_tasklist；CF：=True；TF：=False|}

n：Suspend<>Running

(iftaskstate_decRunningRunningthen1else0)=1

(7)destruct (taskstate_dec Running Running)

分情況討論，比較Running和Running，此時又引入了一個新的條件e，同時證明目標(biāo)被分解為兩個子目標(biāo)，要依次驗證這兩個子目標(biāo).

2subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

n：Suspend<>Running

e：Running=Running

1=1

0=1

(8)reflexivity

子目標(biāo)1要證明1=1，顯式相等得證，消除掉子目標(biāo)1.此時的條件e變?yōu)闂l件n0.

1subgoal

init_state：Rdata

H：init_state={|TL：=init_tasklist；CF：=True；TF：=False|}

n：Suspend<>Running

n0：Running<>Running

0=1

(9)contradiction

子目標(biāo)的前置條件中，Running<>Running，和實際相悖，因此才得到了0=1的錯誤結(jié)論.反證得之，消除子目標(biāo)2，至此證明完畢，初始狀態(tài)滿足性質(zhì)1.

Nomoresubgoal

5 結(jié) 論

本文針對某航天器操作系統(tǒng)SpaceOS2需求層的形式化驗證，首先確定操作系統(tǒng)需求，并由此提煉出六條核心的全局性質(zhì)；然后利用有限狀態(tài)機(jī)方法進(jìn)行形式化描述，建立了一個事件驅(qū)動任務(wù)轉(zhuǎn)移系統(tǒng)模型；最后在定理證明器Coq中形式化定義全局性質(zhì)，并驗證建立的形式化模型是否滿足提出的全局性質(zhì).結(jié)果證明SpaceOS2在需求層滿足提出的全局性質(zhì)，也說明采用有限狀態(tài)機(jī)方法對操作系統(tǒng)需求層進(jìn)行形式化驗證是可行的，為進(jìn)一步全面形式化驗證奠定了基礎(chǔ).