本文關(guān)鍵詞：VTOS內(nèi)存管理的設(shè)計(jì)實(shí)現(xiàn)及其形式化驗(yàn)證研究，由筆耕文化傳播整理發(fā)布。

【摘要】：計(jì)算機(jī)技術(shù)的發(fā)展使得計(jì)算機(jī)的應(yīng)用領(lǐng)域日益擴(kuò)大。在航天航空、軌道交通、醫(yī)療和金融等領(lǐng)域都可看見(jiàn)計(jì)算機(jī)的身影。計(jì)算機(jī)軟件是計(jì)算機(jī)的靈魂,因此現(xiàn)代社會(huì)對(duì)計(jì)算機(jī)軟件的依賴程度非常高。這種局面對(duì)軟件的可靠性提出了很高的要求,社會(huì)對(duì)軟件的高度依賴需要保證軟件高度可靠。操作系統(tǒng)作為部署在計(jì)算機(jī)硬件之上的第一層軟件,其可靠性至關(guān)重要,是其他軟件可靠性的基礎(chǔ)。傳統(tǒng)的軟件工程方法如測(cè)試等無(wú)法完全保證軟件可靠,目前公認(rèn)的能夠保證軟件正確可靠的技術(shù)是形式化驗(yàn)證技術(shù)。因此學(xué)習(xí)期間參加的項(xiàng)目組致力于開(kāi)發(fā)一個(gè)基于微內(nèi)核的操作系統(tǒng)VTOS (Verified Trusted Operating System),使用形式化驗(yàn)證技術(shù)保證其正確性。微內(nèi)核具有封閉性的特點(diǎn),且其小巧性使得形式化描述和驗(yàn)證成為可能。本文研究了VTOS中內(nèi)存管理的設(shè)計(jì)實(shí)現(xiàn)及形式化驗(yàn)證方法,主要貢獻(xiàn)如下：1、設(shè)計(jì)實(shí)現(xiàn)了VTOS的存儲(chǔ)管理。在綜合考慮微內(nèi)核架構(gòu)和系統(tǒng)的性能之后,提出并實(shí)現(xiàn)了將內(nèi)存管理置于系統(tǒng)任務(wù)中的方案。按照功能將內(nèi)存管理劃分為頁(yè)框分配器和進(jìn)程虛存管理兩個(gè)子模塊。頁(yè)框分配器負(fù)責(zé)頁(yè)框的分配和釋放,進(jìn)程虛存管理負(fù)責(zé)管理進(jìn)程的虛擬地址空間。2. VTOS內(nèi)存管理模塊的形式化建模。在考慮并發(fā)的情況下,利用非確定性自動(dòng)機(jī)對(duì)實(shí)現(xiàn)的VTOS內(nèi)存管理模塊進(jìn)行形式化建模,使用Hoare三元組描述了每一個(gè)接口函數(shù)的語(yǔ)義。函數(shù)的語(yǔ)義作為驗(yàn)證的目標(biāo)。3、形式化模型的Isabelle/HOL描述。在輔助定理證明器Isabelle/HOL中描述了為內(nèi)存模塊所建立的自動(dòng)機(jī)模型：定義了模型的狀態(tài)空間；定義了每一個(gè)接口函數(shù)的前置條件和后置條件。為驗(yàn)證奠定了基礎(chǔ)。4, VTOS內(nèi)存管理模塊的形式化驗(yàn)證。對(duì)內(nèi)存管理模塊的形式化驗(yàn)證進(jìn)行了探索,在認(rèn)識(shí)到面向確定性自動(dòng)機(jī)的驗(yàn)證方法不能解決并發(fā)問(wèn)題后,給出了面向非確定性自動(dòng)機(jī)的驗(yàn)證方法。使用新方法對(duì)頁(yè)框釋放函數(shù)free_pages做了驗(yàn)證嘗試,總結(jié)了驗(yàn)證工作所獲得的經(jīng)驗(yàn)。
【關(guān)鍵詞】：操作系統(tǒng) 微內(nèi)核 內(nèi)存管理 模塊化 形式化驗(yàn)證
【學(xué)位授予單位】：南京大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2014
【分類號(hào)】：TP333.1;TP311.52
【目錄】：

• 摘要4-5
• ABSTRACT5-12
• 第一章 緒論12-18
• 1.1 研究背景12-13
• 1.2 相關(guān)工作13-16
• 1.2.1 微內(nèi)核13-14
• 1.2.2 操作系統(tǒng)的形式化驗(yàn)證14-16
• 1.3 本文工作16
• 1.4 內(nèi)容安排16-18
• 第二章 VTOS內(nèi)存模塊的設(shè)計(jì)與實(shí)現(xiàn)18-33
• 2.1 VTOS的結(jié)構(gòu)18-19
• 2.2 內(nèi)存管理模塊的設(shè)計(jì)19-23
• 2.3 頁(yè)框分配器的實(shí)現(xiàn)23-26
• 2.3.1 數(shù)據(jù)對(duì)象23-25
• 2.3.2 接口函數(shù)25-26
• 2.4 進(jìn)程虛存管理的實(shí)現(xiàn)26-32
• 2.4.1 數(shù)據(jù)對(duì)象27-29
• 2.4.2 接口函數(shù)29-32
• 2.5 本章小結(jié)32-33
• 第三章 內(nèi)存模塊的形式化建模33-61
• 3.1 建模方法33-37
• 3.1.1 并發(fā)與非確定性33-35
• 3.1.2 概念與工具35-36
• 3.1.3 模塊化原則36-37
• 3.2 頁(yè)框分配器的建模37-47
• 3.2.1 模型的數(shù)學(xué)語(yǔ)言描述37-42
• 3.2.2 模型的Isabelle/HOL描述42-47
• 3.3 進(jìn)程虛存管理的建模47-60
• 3.3.1 模型的數(shù)學(xué)語(yǔ)言描述47-55
• 3.3.2 模型的Isabelle/HOL描述55-60
• 3.4 本章小結(jié)60-61
• 第四章 內(nèi)存模塊的形式化驗(yàn)證61-84
• 4.1 原驗(yàn)證方法及其存在的問(wèn)題61-64
• 4.2 匯編級(jí)模型與狀態(tài)映射64-71
• 4.2.1 匯編級(jí)模型的定義64-68
• 4.2.2 匯編級(jí)狀態(tài)到抽象自動(dòng)機(jī)狀態(tài)的映射68-70
• 4.2.3 模型之間的同構(gòu)性70-71
• 4.3 函數(shù)的驗(yàn)證71-81
• 4.3.1 函數(shù)的證明思路71-77
• 4.3.2 函數(shù)實(shí)現(xiàn)到Isabelle/HOL的翻譯77-79
• 4.3.3 函數(shù)實(shí)現(xiàn)的正確性驗(yàn)證79-81
• 4.4 本章小結(jié)81-84
• 第五章 總結(jié)與展望84-85
• 5.1 總結(jié)84
• 5.2 展望84-85
• 致謝85-86
• 參考文獻(xiàn)86-88

【共引文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前3條

1 QIAN Zhenjiang;LIU Wei;HUANG Hao;;Research on Microkernel Integrity Semantics Model and Formal Verification[J];Chinese Journal of Electronics;2014年01期

2 王若川;楊孟飛;喬磊;;基于時(shí)間自動(dòng)機(jī)的操作系統(tǒng)中斷管理建模與驗(yàn)證[J];空間控制技術(shù)與應(yīng)用;2014年04期

3 譚彥亮;楊樺;喬磊;;基于Event-B的SpaceOS2操作系統(tǒng)任務(wù)管理需求形式化建模與驗(yàn)證[J];空間控制技術(shù)與應(yīng)用;2014年04期

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前1條

1 錢(qián)振江;安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D];南京大學(xué);2013年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前2條

1 閆鑫;基于ARINC653標(biāo)準(zhǔn)的分區(qū)操作系統(tǒng)隔離性的驗(yàn)證研究[D];太原理工大學(xué);2014年

2 官水旺;VTOS系統(tǒng)任務(wù)設(shè)計(jì)與形式化驗(yàn)證[D];南京大學(xué);2014年

  本文關(guān)鍵詞：VTOS內(nèi)存管理的設(shè)計(jì)實(shí)現(xiàn)及其形式化驗(yàn)證研究，，由筆耕文化傳播整理發(fā)布。

本文編號(hào)：442711