系統(tǒng)軟件是計(jì)算機(jī)系統(tǒng)的核心部分,其安全性和可靠性是構(gòu)建高可信計(jì)算機(jī)系統(tǒng)的關(guān)鍵。而形式化驗(yàn)證技術(shù)基于嚴(yán)格的數(shù)學(xué)理論和方法,能夠?yàn)橄到y(tǒng)軟件的正確性提供強(qiáng)有力的保證。在系統(tǒng)軟件中,內(nèi)嵌匯編代碼常被用于實(shí)現(xiàn)與底層硬件平臺(tái)之間的交互。匯編代碼的安全性和正確性對(duì)于保證整個(gè)系統(tǒng)的正確性是非常重要的。在某航天嵌入式操作系統(tǒng)的形式化驗(yàn)證工作項(xiàng)目中,該操作系統(tǒng)的內(nèi)嵌匯編程序是由SPARCv8指令集編寫(xiě)的,而項(xiàng)目前期工作所采用的驗(yàn)證框架,無(wú)法驗(yàn)證這部分內(nèi)嵌匯編程序的正確性。為了完善這一部分工作,本文基于己有的形式化驗(yàn)證技術(shù)提出了一套用于SPARCv8匯編程序驗(yàn)證的方法,并做出了如下貢獻(xiàn):首先,本文為SPARCv8匯編程序設(shè)計(jì)了一種霍爾風(fēng)格的驗(yàn)證邏輯。并為驗(yàn)證邏輯中的推理規(guī)則提供了直接風(fēng)格的（direct-style）、基于語(yǔ)義的解釋。該驗(yàn)證邏輯支持SPARCv8匯編程序中函數(shù)調(diào)用的模塊化驗(yàn)證,以及SPARCv8的三個(gè)特性的驗(yàn)證:包括延時(shí)跳轉(zhuǎn)、特殊寄存器的延時(shí)寫(xiě)入和寄存器窗口機(jī)制。其次,應(yīng)用所設(shè)計(jì)的驗(yàn)證邏輯,本文驗(yàn)證了某航天嵌入式操作系統(tǒng)中任務(wù)上下文切換程序的主要功能模塊,累計(jì)共驗(yàn)證了約250行SPARCv8... 

【文章來(lái)源】：中國(guó)科學(xué)技術(shù)大學(xué)安徽省 211工程院校 985工程院校

【文章頁(yè)數(shù)】：111 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

圖３．１?ＳＰＡＲＣｖ８程序機(jī)器模型??

刁寄存搖

定義了斷言語(yǔ)言之后，我們?cè)谶@一節(jié)開(kāi)始介紹推理規(guī)則的設(shè)計(jì)，設(shè)計(jì)推理規(guī)??則的目的是為了證明程序滿足其所對(duì)應(yīng)的程序規(guī)范。所以，我們首先從程序規(guī)范??入手通過(guò)圖４．３來(lái)向讀者闡釋我們驗(yàn)證邏輯中程序規(guī)范的定義。??（Ｓｐｅｃ）?＾?：：＝?｛ｆ?＾??ｆｉ：?＾１??１１??ｆ２：?０２??１２??０３１??Ｉｓ??代碼堆Ｃ??圖４．３驗(yàn)證邏輯程序規(guī)范??２６??


本文編號(hào)：3376757