羅爾聰,郭 宇

(1.中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,合肥230026;

2.中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室,江蘇蘇州215123)

μC/OS-Ⅲ任務(wù)調(diào)度器在Coq中的驗(yàn)證

羅爾聰1,2,郭 宇1,2

(1.中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,合肥230026;

2.中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室,江蘇蘇州215123)

以μC/OS-Ⅲ內(nèi)核中的任務(wù)調(diào)度器為研究對(duì)象,選取調(diào)度相關(guān)的核心代碼,驗(yàn)證調(diào)度器代碼滿足優(yōu)先調(diào)度最高優(yōu)先級(jí)任務(wù)的性質(zhì)?；诜蛛x邏輯與SCAP驗(yàn)證理論,利用Coq輔助證明工具,通過(guò)定義機(jī)器模型、操作語(yǔ)義、邏輯斷言以及推導(dǎo)規(guī)則構(gòu)建驗(yàn)證框架。在驗(yàn)證框架中,定義內(nèi)核數(shù)據(jù)結(jié)構(gòu)和內(nèi)核相關(guān)性質(zhì)的邏輯描述,模塊化地對(duì)內(nèi)核代碼進(jìn)行推理。驗(yàn)證結(jié)果表明,μC/OS-Ⅲ任務(wù)調(diào)度器滿足可靠性要求,并且可以通過(guò)機(jī)器的自動(dòng)檢查。

任務(wù)調(diào)度器;形式化驗(yàn)證;分離邏輯;Coq證明工具;最高優(yōu)先級(jí)

1 概述

嵌入式操作系統(tǒng)負(fù)責(zé)管理系統(tǒng)軟硬件資源,在工業(yè)控制、移動(dòng)設(shè)備等領(lǐng)域中處于非常關(guān)鍵的位置。為確保這部分完成任務(wù)調(diào)度的代碼能夠正確地運(yùn)行,本文采用邏輯驗(yàn)證的形式化方法,在輔助證明工具Coq［1］中驗(yàn)證μC/OS-Ⅲ［2］內(nèi)核中的任務(wù)調(diào)度器代碼。μC/OS-Ⅲ任務(wù)調(diào)度器的形式化工作主要有以下難點(diǎn):

(1)調(diào)度器代碼涉及到諸多系統(tǒng)數(shù)據(jù)結(jié)構(gòu),驗(yàn)證之前需要描述其系統(tǒng)數(shù)據(jù)結(jié)構(gòu)的性質(zhì)和它們相互之間應(yīng)該滿足的關(guān)系。

(2)任務(wù)(Task),作為操作系統(tǒng)中運(yùn)行的基本單元,具有描述其重要程度的優(yōu)先級(jí)(Priority)屬性。在任務(wù)調(diào)度過(guò)程中,內(nèi)核需要完成對(duì)最高優(yōu)先級(jí)(Highest Priority)任務(wù)的選取,然后進(jìn)行任務(wù)上下文切換。驗(yàn)證需要保證在執(zhí)行調(diào)度函數(shù)代碼前后,內(nèi)核中描述任務(wù)優(yōu)先級(jí)的變量能夠正確讀寫(xiě)。

本文從μC/OS-Ⅲ任務(wù)調(diào)度器選取相關(guān)代碼,將其編譯后的匯編級(jí)指令進(jìn)行形式化建模,然后為這部分指令給出形式化的規(guī)范(Specification)描述,并證明這部分代碼滿足最高優(yōu)先級(jí)調(diào)度性質(zhì):從任意一個(gè)合法機(jī)器狀態(tài)集合出發(fā),任務(wù)調(diào)度程序執(zhí)行調(diào)度相關(guān)代碼,之后到達(dá)一個(gè)新的狀態(tài)。在這個(gè)新?tīng)顟B(tài)中,相關(guān)

全局變量記錄正確的最高優(yōu)先級(jí)與被選任務(wù)。

本文驗(yàn)證的內(nèi)核調(diào)度代碼基于一個(gè)形式化的簡(jiǎn)化機(jī)器模型,采用分離邏輯［3］描述內(nèi)核規(guī)范,同時(shí)采用SCAP［4］邏輯對(duì)內(nèi)核指令進(jìn)行推理。本文的所有形式化工作都基于交互式定理證明工具Coq,主要工作如下:

(1)驗(yàn)證μC/OS-Ⅲ任務(wù)調(diào)度器相關(guān)代碼以下關(guān)鍵性質(zhì)(內(nèi)存安全性、部分指令代碼的功能正確性和最高優(yōu)先級(jí))。

(2)使用證明輔助工具Coq實(shí)現(xiàn)邏輯系統(tǒng)和驗(yàn)證選取代碼,所有定義和證明都可以接受機(jī)器自動(dòng)檢查。

2 相關(guān)工作

文獻(xiàn)［5］提出了一種基于C語(yǔ)言的FreeRTOS任務(wù)調(diào)度器的自動(dòng)化證明方法。本文統(tǒng)一使用匯編語(yǔ)言進(jìn)行建模,使得程序斷言能夠?qū)崿F(xiàn)對(duì)機(jī)器狀態(tài)的精確描述,且稍加擴(kuò)展便可驗(yàn)證操作系統(tǒng)底層代碼。

使用Coq交互式驗(yàn)證工作量巨大,文獻(xiàn)［6-7］提供了可供參考的自動(dòng)化或半自動(dòng)化驗(yàn)證策略。文獻(xiàn)［8］以SCAP框架為基礎(chǔ)提出一種含有模擬關(guān)系的虛擬機(jī)構(gòu)造和驗(yàn)證方案,可以作為本文改進(jìn)的借鑒。

3 驗(yàn)證方法

本文選取μC/OS-Ⅲ任務(wù)調(diào)度器中的2個(gè)重要函數(shù)OSSched()和OSIntExit()進(jìn)行實(shí)現(xiàn)代碼級(jí)驗(yàn)證。本節(jié)介紹它們所涉及的內(nèi)核數(shù)據(jù)結(jié)構(gòu)及其執(zhí)行流程。

3.1 系統(tǒng)就緒表與系統(tǒng)優(yōu)先級(jí)表

在μC/OS-Ⅲ中,任務(wù)通過(guò)任務(wù)控制塊(TCB)來(lái)描述其狀態(tài)。TCB含有前向指針、后向指針和優(yōu)先級(jí)3個(gè)域。通過(guò)前2個(gè)域,優(yōu)先級(jí)相同的TCB構(gòu)成雙鏈表。系統(tǒng)就緒表將分離的具有不同優(yōu)先級(jí)的TCB雙鏈表組織起來(lái),在內(nèi)存中由一個(gè)全局的一維數(shù)組表示。數(shù)組元素由頭指針、尾指針和元素計(jì)數(shù)3個(gè)域構(gòu)成,如圖1所示。

圖1 系統(tǒng)就緒表與系統(tǒng)優(yōu)先級(jí)表

系統(tǒng)優(yōu)先級(jí)表是另外一個(gè)全局一維數(shù)組,其設(shè)立的目的是為了快速獲得系統(tǒng)就緒表中的狀態(tài),數(shù)組元素取值與系統(tǒng)就緒表中對(duì)應(yīng)TCB雙鏈表元素?cái)?shù)量相關(guān)。

為了確保調(diào)度過(guò)程的正確執(zhí)行,調(diào)度代碼對(duì)兩表進(jìn)行操作時(shí)必須滿足以下4個(gè)關(guān)鍵性質(zhì):

性質(zhì)1(良形雙鏈表) 雙鏈表中的每一個(gè)節(jié)點(diǎn)都正確地指向其前驅(qū)和后繼節(jié)點(diǎn),此外雙鏈表中的TCB還擁有共同的優(yōu)先級(jí)。本文將此類雙鏈表稱之為良形雙鏈表。

性質(zhì)2(良形系統(tǒng)就緒表數(shù)組元素) 以良形雙鏈表共同優(yōu)先級(jí)為系統(tǒng)就緒表索引,獲得的數(shù)組元素的頭指針指向雙鏈表隊(duì)首,尾指針指向雙鏈表隊(duì)尾,元素計(jì)數(shù)與雙鏈表中TCB數(shù)量相等。本文稱之為良形數(shù)組元素。

性質(zhì)3(系統(tǒng)就緒表與系統(tǒng)優(yōu)先級(jí)表的一致性)

以系統(tǒng)就緒表任意數(shù)組元素都是良形為前提,對(duì)于任意索引,指向雙鏈表的元素?cái)?shù)量與系統(tǒng)優(yōu)先級(jí)表對(duì)應(yīng)元素取值存在雙射關(guān)系:元素?cái)?shù)量為0(不為0),當(dāng)且僅當(dāng)系統(tǒng)優(yōu)先級(jí)表對(duì)應(yīng)元素為0(為1)。本文稱之為一致性。

性質(zhì)4(最高優(yōu)先級(jí)) 優(yōu)先級(jí)p是最高優(yōu)先級(jí),當(dāng)且僅當(dāng)系統(tǒng)就緒表中索引為p的數(shù)組元素指向的雙鏈表元素?cái)?shù)量不為0(系統(tǒng)優(yōu)先級(jí)表對(duì)應(yīng)元素為1),索引小于p的數(shù)組元素指向的雙鏈表元素?cái)?shù)量為0(系統(tǒng)優(yōu)先級(jí)表對(duì)應(yīng)元素為0)。

3.2 任務(wù)調(diào)度函數(shù)驗(yàn)證

函數(shù)OSSched()和OSIntExit()是任務(wù)調(diào)度器的核心代碼,前者實(shí)現(xiàn)任務(wù)級(jí)任務(wù)調(diào)度,后者實(shí)現(xiàn)中斷級(jí)任務(wù)調(diào)度。OSSched()在任務(wù)實(shí)現(xiàn)代碼里被主動(dòng)調(diào)用,OSSched與OSIntExit的函數(shù)流程如下:

函數(shù)入口是一系列任務(wù)調(diào)度條件判斷語(yǔ)句,以及關(guān)中斷進(jìn)入臨界區(qū)的指令,之后函數(shù)通過(guò)系統(tǒng)優(yōu)

先級(jí)表和系統(tǒng)就緒表分別獲取最高優(yōu)先級(jí)與待切換任務(wù),最后在退出臨界區(qū)之前進(jìn)行任務(wù)級(jí)上下文切換。OSIntExit()通常在系統(tǒng)中斷服務(wù)程序中被調(diào)用,函數(shù)主體都在臨界區(qū)內(nèi)。

對(duì)比上述執(zhí)行流程可知,2個(gè)函數(shù)采用相同代碼實(shí)現(xiàn)獲取最高優(yōu)先級(jí)與待切換任務(wù)。在形式化過(guò)程中,性質(zhì)3描述的一致性是這段代碼正確性的保證。同時(shí)驗(yàn)證被調(diào)用的OS_PrioGetHighest()函數(shù)時(shí)需要使用性質(zhì)4的內(nèi)容。

4 硬件機(jī)器模型與推理邏輯系統(tǒng)

本文選取Intel i386架構(gòu)的一個(gè)簡(jiǎn)化子集作為運(yùn)行μC/OS-Ⅲ內(nèi)核的硬件平臺(tái),并采用程序邏輯SCAP推理本文所研究的任務(wù)調(diào)度器代碼。

4.1 機(jī)器模型與操作語(yǔ)義

機(jī)器配置(mach)在Coq中被定義為四元組:

其中,代碼code是地址到機(jī)器指令的映射;內(nèi)存mem是地址到機(jī)器字的映射,寄存器文件regfile是從寄存器到機(jī)器字的映射;pc表示指令指針。

Inductive reg:Set:=eax:reg|edx:reg|ebp:reg|esp:reg |irf:reg|zf:reg.

注意這里的寄存器不僅包括通用寄存器eax和edx等,還包含一個(gè)中斷寄存器irf和獨(dú)立的標(biāo)志位寄存器zf。在Coq中,寄存器通過(guò)歸納定義reg實(shí)現(xiàn)。

機(jī)器模型中指令集是i386機(jī)器指令集的一個(gè)子集,包含常見(jiàn)的指令,包括移位、算數(shù)、比較等指令。在Coq中,指令instruction也采用歸納定義:

指令的執(zhí)行指令語(yǔ)義采用2個(gè)關(guān)系謂詞來(lái)定義,NextS與NextPC。前者描述在指令執(zhí)行前后,內(nèi)存與寄存器的改變,而后者描述控制流的走向。

以MOV指令為例,謂詞NextS首先從寄存器文件R中獲取寄存器單元rs的值,暫存到變量x,然后通過(guò)函數(shù)rf_update更新R中的rd寄存器,新的寄存器文件為R′。

謂詞NextPC定義了指令指針的變化:在執(zhí)行MOV指令之后,指令指針加一,指向下一條指令。

限于篇幅,這里不再贅述其余的指令。其形式化語(yǔ)義大部分遵守Intel手冊(cè)中的描述。

4.2 斷言語(yǔ)言與推理邏輯系統(tǒng)

為了描述函數(shù)規(guī)范,本文采用分離邏輯的斷言語(yǔ)言來(lái)描述。后文中將要使用到的部分邏輯連接詞如下:

其中,p??q表示分離合取;為了描述不依賴于任何存儲(chǔ)的斷言,本文用!標(biāo)記純斷言(pure assertion); l|-＞w表示地址為l的內(nèi)存單元存儲(chǔ)值為w。在Coq實(shí)現(xiàn)時(shí),本文采用淺嵌入［9］的方式來(lái)定義斷言語(yǔ)言。

程序邏輯SCAP(Stack-based Certified Assembly Language)是用來(lái)推理帶有結(jié)構(gòu)化堆棧操作的機(jī)器指令的類似Hoare邏輯［10］的推理系統(tǒng)。SCAP邏輯的推理過(guò)程以指令序列為單位。函數(shù)由一些指令序列構(gòu)成,程序規(guī)范以函數(shù)為單位定義。程序規(guī)范是一個(gè)二元組,包含一個(gè)前條件與一個(gè)描述函數(shù)前后狀態(tài)變化的二元關(guān)系:

程序規(guī)范集合PSpec是一個(gè)從一個(gè)指令序列的起始地址到函數(shù)規(guī)范的定義。下面列出SCAP推理規(guī)則在Coq中的定義框架:

可以看出,推理規(guī)則被定義成一個(gè)多元關(guān)系WFcomm,根據(jù)接受的指令進(jìn)行分情況展開(kāi),每一個(gè)分支對(duì)應(yīng)不同指令的推導(dǎo)規(guī)則。

5 驗(yàn)證實(shí)現(xiàn)

本節(jié)介紹符合性質(zhì)1和性質(zhì)2的內(nèi)核數(shù)據(jù)結(jié)構(gòu),以及符合性質(zhì)3和性質(zhì)4的內(nèi)核性質(zhì)的斷言構(gòu)

造過(guò)程。

5.1 內(nèi)核數(shù)據(jù)結(jié)構(gòu)的表示

為表示相同元素組成的有序序列,本文以Coq標(biāo)準(zhǔn)庫(kù)中多態(tài)list作為形式化的基礎(chǔ)歸納構(gòu)造類型,以實(shí)現(xiàn)核心數(shù)據(jù)與特定數(shù)據(jù)結(jié)構(gòu)的分離。以圖1中OSPrioTbl索引0～4的片段為例,定義抽象優(yōu)先級(jí)表如下:

Definition l:list TID:=(0::0::1::1::0::nil).

由前文可知系統(tǒng)就緒表中TCB存在2種序關(guān)系:優(yōu)先級(jí)上有序和優(yōu)先級(jí)內(nèi)有序。因此,本文以list復(fù)合構(gòu)建抽象系統(tǒng)就緒表。圖1中OSRdyList索引0～4片段的具體定義如下所示(設(shè)TCB地址為1～5):

在定義抽象內(nèi)核數(shù)據(jù)之后,本文通過(guò)4個(gè)步驟實(shí)現(xiàn)針對(duì)μC/OS-Ⅲ系統(tǒng)特定數(shù)據(jù)結(jié)構(gòu)斷言的構(gòu)造。

(1)TCB斷言。其中,PrevPtr,NextPtr和Prio為相對(duì)TCB起始地址的偏移常量。任意TCB起始地址不能為0。

(2)良形雙鏈表斷言。根據(jù)性質(zhì)1描述,通過(guò)具有同一優(yōu)先級(jí)的抽象系統(tǒng)就緒表進(jìn)行歸納構(gòu)造:

(3)良形系統(tǒng)就緒表數(shù)組元素?cái)嘌?。根?jù)性質(zhì)2描述進(jìn)行構(gòu)造,其中函數(shù)length的作用是返回list長(zhǎng)度。

(4)系統(tǒng)就緒表斷言。參數(shù)p為系統(tǒng)就緒表內(nèi)存起始地址(相鄰單元地址偏移為12),參數(shù)ll為抽象系統(tǒng)就緒表,參數(shù)prio為優(yōu)先級(jí)迭代的起始值,通常為0。

系統(tǒng)優(yōu)先級(jí)表斷言的定義過(guò)程與系統(tǒng)就緒表類似,在此不再贅述。

5.2 內(nèi)核性質(zhì)的表示

性質(zhì)3描述了具有同一索引的系統(tǒng)就緒表數(shù)組元素與系統(tǒng)優(yōu)先級(jí)表元素的一一映射關(guān)系。利用上一節(jié)定義的抽象內(nèi)核數(shù)據(jù),本文采用斷言函數(shù)Correspondence描述一致性:

Correspondence的核心規(guī)則是當(dāng)兩表不為空時(shí),取得各表頭元素,遞歸構(gòu)造滿足性質(zhì)3的合取范式。根據(jù)性質(zhì)4,本文通過(guò)函數(shù)HighestPriority實(shí)現(xiàn)優(yōu)先級(jí)p是否為抽象系統(tǒng)就緒表最高優(yōu)先級(jí)的判斷:

HighestPriority本質(zhì)為系統(tǒng)就緒表從O～p索引元素?cái)嘌缘暮先》妒?。同?本文構(gòu)造系統(tǒng)優(yōu)先級(jí)表的最高優(yōu)先級(jí)斷言函數(shù)HighestPriorityHash如下:

以上描述內(nèi)核性質(zhì)的3個(gè)斷言函數(shù),滿足關(guān)系如下:

引理1 對(duì)于任意抽象系統(tǒng)就緒表與系統(tǒng)優(yōu)先級(jí)表,若滿足一致性,那么對(duì)于任意優(yōu)先級(jí)p,它是系統(tǒng)就緒表最高優(yōu)先級(jí)當(dāng)且僅當(dāng)亦是系統(tǒng)優(yōu)先級(jí)表最高優(yōu)先級(jí)。

證明過(guò)程略。

此外,本文還定義了判斷某一TCB是否在抽象系統(tǒng)就緒表中的斷言函數(shù)InRL:

InRL本質(zhì)為依次對(duì)每個(gè)元素判斷的析取范式。存在關(guān)系斷言與系統(tǒng)就緒表最高優(yōu)先級(jí)斷言存在如下關(guān)系:

引理2 對(duì)于任意TCB與抽象系統(tǒng)就緒表,如果TCB存在于抽象系統(tǒng)就緒表中,那么此抽象系統(tǒng)就緒表存在最高優(yōu)先級(jí)。

5.3 內(nèi)核實(shí)現(xiàn)代碼的推理

本文3.2節(jié)中兩函數(shù)共有的調(diào)度代碼(下劃線部分),轉(zhuǎn)換成匯編指令后形式化推理過(guò)程如下:

調(diào)度代碼的推理過(guò)程如下:

關(guān)于調(diào)度代碼的驗(yàn)證工作,有以下3點(diǎn)需要補(bǔ)充說(shuō)明:

(1)當(dāng)前任務(wù)指針和當(dāng)前優(yōu)先級(jí)分別由全局變量OSTCBCurPtr和OSPrioCur記錄,被選取的任務(wù)指針和最高優(yōu)先級(jí)分別由全局變量OSTCBHighRdyPtr和

OSPrioHighRdy記錄。對(duì)比調(diào)度代碼執(zhí)行前后斷言可以發(fā)現(xiàn)后兩者的變化。

(2)斷言函數(shù)K描述任務(wù)棧上的存儲(chǔ),有3個(gè)參數(shù):第1個(gè)參數(shù)為基地址b,第2個(gè)和第3個(gè)參數(shù)都為list。其功能是分別將兩list映射到b-4n至b-4和b至b+4(m-1)的內(nèi)存地址空間(n,m分別為兩list長(zhǎng)度)。

(3)函數(shù)OS_PrioGetHighest()獲取最高優(yōu)先級(jí),保存在eax寄存器中返回。以一致性和存在關(guān)系為前提,OS_PrioGetHighest()前斷言中的系統(tǒng)優(yōu)先級(jí)表最高優(yōu)先級(jí)性質(zhì)可以通過(guò)引理1、引理2推導(dǎo)出來(lái)。

5.4 驗(yàn)證結(jié)果

根據(jù)以上內(nèi)容,本文形式化定義并驗(yàn)證了最高優(yōu)先級(jí)調(diào)度性質(zhì)如下:

以本文定義的機(jī)器模型為基礎(chǔ),從任一滿足一致性與存在性質(zhì)的合法狀態(tài)(C,M,R,pc)出發(fā),系統(tǒng)在運(yùn)行任務(wù)調(diào)度相關(guān)代碼后,到達(dá)一個(gè)新?tīng)顟B(tài)(C,M′,R′,pc′),新?tīng)顟B(tài)里全局變量OSPrioHighRdy記錄最高優(yōu)先級(jí),全局指針OSTCBHighRdyPtr記錄待切換的TCB。

除此之外,本文還形式化驗(yàn)證了內(nèi)存安全性、部分指令代碼的功能正確性,以及推理規(guī)則可靠性等性質(zhì)。表1展示了本文驗(yàn)證的內(nèi)核調(diào)度函數(shù)列表。整個(gè)證明工作共花費(fèi)數(shù)月時(shí)間,Coq代碼總量為5萬(wàn)多行。

表1 內(nèi)核調(diào)度相關(guān)函數(shù)

6 結(jié)束語(yǔ)

操作系統(tǒng)任務(wù)調(diào)度器由于其結(jié)構(gòu)復(fù)雜是驗(yàn)證工作難點(diǎn)。本文以嵌入式內(nèi)核μC/OS-Ⅲ的任務(wù)調(diào)度器為研究對(duì)象,基于相關(guān)框架和模型,利用Coq輔助證明工具,最終形式化驗(yàn)證了調(diào)度代碼滿足相關(guān)性質(zhì),并且得到可以經(jīng)過(guò)機(jī)器自動(dòng)檢查的證明。

本文對(duì)μC/OS-Ⅲ任務(wù)調(diào)度器的關(guān)注重點(diǎn)集中在最高優(yōu)先級(jí)如何被正確選取,利用文獻(xiàn)［11］提出的相關(guān)邏輯和文獻(xiàn)［12］提出的上下文切換驗(yàn)證框架,將μC/OS-Ⅲ任務(wù)級(jí)和中斷級(jí)上下文切換整合進(jìn)μC/OS-Ⅲ任務(wù)調(diào)度器形式化工作,是下一步的研究方向。

［1]Micriμm.μC/OS-Ⅲ用戶手冊(cè)［EB/OL］.［2014-05-01］.https://doc.micrium.com/pages/viewpage.action?pageId= 10753180.

［2]Coq開(kāi)發(fā)團(tuán)隊(duì).Coq證明輔助工具參考手冊(cè)［EB/OL］.［2014-05-01］.http://coq.inria.fr.

［3]Reynolds J C.Separation Logic:A Logic for Shared Mutable Data Structures［C］//Proceedings of the 17th AnnualIEEESymposiumonLogicinComputer Science.［S.l.］:IEEE Computer Society,2002:55-74.

［4]Feng X,Shao Z,Vaynberg A,et al.Modular Verification of Assembly Code with Stack-based Control Abstractions［J］.ACMSIGPLANNotices,2006,41(6): 401-414.

［5]Ferreira J F,He G,Qin S.Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK［C］//Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering.［S.l.］:IEEE Press,2012:51-58.

［6]Berdine J,CalcagnoCO,HearnPW.Symbolic Execution with Separation Logic［M］//Jhala R,Igarashi A.ProgrammingLanguagesandSystems.Berlin, Germany:Springer,2005:52-68.

［7]McCreight A.Practical Tactics for Separation Logic［M］// Seidenberg A.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2009:343-358.

［8]董 淵,任 愷,王生原,等.字節(jié)碼虛擬機(jī)的構(gòu)造和驗(yàn)證［J］.軟件學(xué)報(bào),2010,21(2):305-317.

［9]Garillot F,Werner B.Simple Types in Type Theory: Deep andShallowEncodings［M］//SchneiderK, Brandt J.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2007:368-382.

［10]Hoare C A R.AnAxiomaticBasisforComputer Programming［J］.Communications of the ACM,1969, 12(10):576-580.

［11]Feng X,Shao Z,Dong Y,et al.Certifying Low-level Programs withHardwareInterruptsandPreemptive Threads［J］.ACM SIGPLAN Notices,2008,43(6): 170-182.

［12]Guo Y,Feng X,Shao Z,et al.Modular Verification of Concurrent Thread Management［M］//Jhala R,Igarashi A.Programming Languages and Systems.Berlin,Germany: Springer,2012:315-331.

編輯 金胡考

Verification of μC/OS-ⅢTask Scheduler in Coq

LUO Ercong1,2,GUO Yu1,2
(1.College of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China;
2.Software Security Laboratory,Suzhou Institute for Advanced Study, University of Science and Technology of China,Suzhou 215123,China)

This paper studies the task scheduler in a widely used embedded μC/OS-Ⅲkernel.After selecting core parts from the scheduler,it specifies the properties of the scheduler formally.Based on the separation logic and SCAP,it builds a verification framework including a machine model,operational semantics,assertion languages,and inference rules.In the framework,assertions specifying system data structures and properties are defined,and system code is able to be reasoned about modularly.Finally,the properties of the task scheduler in μC/OS-Ⅲare formally proved,and the entire proof provided by the work are machine checkable.

task scheduler;formal verification;separation logic;Coq proof tool;highest priority

羅爾聰,郭 宇.μC/OS-Ⅲ任務(wù)調(diào)度器在Coq中的驗(yàn)證［J］.計(jì)算機(jī)工程,2015,41(3):53-58.

英文引用格式:Luo Ercong,Guo Yu.Verification of μC/OS-ⅢTask Scheduler in Coq［J］.Computer Engineering, 2015,41(3):53-58.

1000-3428(2015)03-0053-06

:A

:TP309

10.3969/j.issn.1000-3428.2015.03.010

國(guó)家自然科學(xué)基金資助青年項(xiàng)目(61202052);國(guó)家自然科學(xué)基金海外及港澳學(xué)者合作研究基金資助項(xiàng)目(61229201)。

羅爾聰(1989-),男,碩士研究生,主研方向:形式化驗(yàn)證,軟件安全;郭 宇,副教授。

2014-05-05

:2014-05-28E-mail:ecluo@mail.ustc.edu.cn