μC-OS-Ⅲ任務(wù)調(diào)度器的驗(yàn)證.pdf

1、近年來隨著嵌入式設(shè)備的日益普及，嵌入式軟件的安全性越發(fā)顯得重要。在一些關(guān)鍵領(lǐng)域，如航天、醫(yī)療、軍事、核能等，如果嵌入式軟件存在程序漏洞，有可能導(dǎo)致程序在非正常狀態(tài)運(yùn)行，從而會帶來災(zāi)難性的后果。為了解決這一類的可靠性問題，傳統(tǒng)軟件開發(fā)者通常會采用軟件測試的方法去發(fā)現(xiàn)程序錯誤。但是，軟件測試無法保證整個系統(tǒng)完全不存在缺陷。程序驗(yàn)證探尋一條邏輯驗(yàn)證為基礎(chǔ)的解決軟件安全性的道路。程序驗(yàn)證能夠克服軟件測試的一些固有缺點(diǎn)，能夠證明程序嚴(yán)格地符合一定

2、的性質(zhì)，從而保證軟件的可靠性。
　　操作系統(tǒng)中的任務(wù)調(diào)度器由于其結(jié)構(gòu)復(fù)雜而難以驗(yàn)證:首先任務(wù)調(diào)度器的代碼涉及到諸多的復(fù)雜內(nèi)核數(shù)據(jù)結(jié)構(gòu)，在驗(yàn)證它們之前需要描述這部分內(nèi)核數(shù)據(jù)結(jié)構(gòu)的性質(zhì)和它們相互之間應(yīng)該滿足的復(fù)雜關(guān)系;此外在任務(wù)調(diào)度過程中，內(nèi)核需要保證調(diào)度策略的正確性，即選取具有最高優(yōu)先級的就緒任務(wù)，然后通過任務(wù)上下文切換來保證高優(yōu)先級的任務(wù)優(yōu)先得到運(yùn)行。
　　本文以μC/OS-Ⅲ內(nèi)核中的任務(wù)調(diào)度器為研究對象，選取與調(diào)度有關(guān)的核

3、心代碼，驗(yàn)證調(diào)度器代碼滿足優(yōu)先調(diào)度最高優(yōu)先級任務(wù)的性質(zhì)。本文基于分離邏輯與SCAP驗(yàn)證理論，利用Coq輔助證明工具，通過定義機(jī)器模型、操作語義、邏輯斷言以及推導(dǎo)規(guī)則等來構(gòu)建驗(yàn)證框架。在驗(yàn)證框架，本文定義了內(nèi)核數(shù)據(jù)結(jié)構(gòu)和“優(yōu)先調(diào)度最高優(yōu)先級”的性質(zhì)的邏輯描述，模塊化地對內(nèi)核代碼進(jìn)行推理，最終的驗(yàn)證結(jié)果保證μC/OS-Ⅲ任務(wù)調(diào)度器的滿足可靠性的要求。
　　本文主要貢獻(xiàn)如下:
　　(1)驗(yàn)證了μC/OS-Ⅲ任務(wù)調(diào)度器中的核心代碼滿