本文關(guān)鍵詞： 操作系統(tǒng) 內(nèi)存管理 形式化設(shè)計(jì) 形式化驗(yàn)證 定理證明　出處：《電子學(xué)報(bào)》2017年01期 　論文類(lèi)型：期刊論文

【摘要】：由于巨大的規(guī)模和復(fù)雜性,操作系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)的正確性很難用傳統(tǒng)的定量方法來(lái)描述.本文闡述對(duì)微內(nèi)核操作系統(tǒng)的形式化設(shè)計(jì)和驗(yàn)證的方法.在匯編層利用非確定性自動(dòng)機(jī)對(duì)系統(tǒng)進(jìn)行形式化建模,并使用Hoare三元組描述模塊接口函數(shù)的前后置條件,作為函數(shù)正確性的定義.以實(shí)現(xiàn)的VSOS(Verified Secure Operating System)內(nèi)存管理模塊為例,在Isabelle/HOL定理證明器環(huán)境中對(duì)建立的內(nèi)存管理模型和系統(tǒng)行為的操作語(yǔ)義進(jìn)行形式化描述,并對(duì)內(nèi)存管理模塊的設(shè)計(jì)和實(shí)現(xiàn)的正確性進(jìn)行驗(yàn)證.結(jié)果表明,這一方法是可行的和高效的.
[Abstract]:Because of its size and complexity, The correctness of the design and implementation of the operating system is difficult to be described by the traditional quantitative method. This paper describes the formal design and verification methods of the microkernel operating system. In the assembly layer, the non-deterministic automata is used to model the system formally. The Hoare triple is used to describe the pre-and post-condition of the module interface function as the definition of the correctness of the function. The VSOS(Verified Secure Operating system memory management module is used as an example. In the Isabelle/HOL theorem prover environment, the established memory management model and the operational semantics of the system behavior are formally described, and the correctness of the design and implementation of the memory management module is verified. This method is feasible and efficient.
【作者單位】： 南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系;常熟理工學(xué)院計(jì)算機(jī)科學(xué)與工程學(xué)院;
【基金】：國(guó)家自然科學(xué)基金(No.61402057) 江蘇省科技計(jì)劃自然科學(xué)研究項(xiàng)目(No.BK20140418) 中國(guó)博士后科學(xué)基金(No.2015M571737) 江蘇省“六大人才高峰”高層次人才項(xiàng)目(No.2011-DZXX-035) 江蘇省高校自然科學(xué)研究項(xiàng)目(No.12KJB520001)
【分類(lèi)號(hào)】：TP316

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 古天龍;董榮勝;;歐洲高校計(jì)算機(jī)專(zhuān)業(yè)的形式化方法課程教學(xué)[J];計(jì)算機(jī)教育;2008年10期

2 柴振榮;《編程中的形式化方法及其應(yīng)用》會(huì)議[J];管理科學(xué)文摘;1995年06期

3 鄭士貴;智能服務(wù)網(wǎng)絡(luò)形式化方法的模擬和實(shí)質(zhì)[J];管理科學(xué)文摘;1997年01期

4 姜利;孫永強(qiáng);;形式化方法的發(fā)展及展望[J];計(jì)算機(jī)科學(xué);1998年02期

5 張廣泉;關(guān)于軟件形式化方法[J];重慶師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2002年02期

6 鹿蕾;;形式化方法B的證明技術(shù)[J];現(xiàn)代電子技術(shù);2005年23期

7 陳澎;設(shè)計(jì)模式形式化方法分析和初步比較[J];計(jì)算機(jī)工程;2005年02期

8 李建華;李紅革;;形式化及其歷史發(fā)展[J];自然辯證法研究;2008年08期

9 曹源;唐濤;徐田華;穆建成;;形式化方法在列車(chē)運(yùn)行控制系統(tǒng)中的應(yīng)用[J];交通運(yùn)輸工程學(xué)報(bào);2010年01期

10 ;《軟件學(xué)報(bào)》形式化方法和工具專(zhuān)刊征文通知[J];軟件學(xué)報(bào);2010年07期

相關(guān)會(huì)議論文 前7條

1 李文健;;形式化的涵義及其認(rèn)識(shí)論本質(zhì)[A];1993年邏輯研究專(zhuān)輯[C];1993年

2 吳允曾;;關(guān)于形式化的幾個(gè)問(wèn)題[A];金岳霖學(xué)術(shù)思想研究——金岳霖學(xué)術(shù)思想研討會(huì)論文集[C];1985年

3 鄭宇軍;石海鶴;薛錦云;;Spec#語(yǔ)言中的形式化特性[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

4 雷敏;雷友殉;;一種UML到SDL轉(zhuǎn)換方法的研究與應(yīng)用[A];2006通信理論與技術(shù)新進(jìn)展——第十一屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集[C];2006年

5 苗潔君;王克;;密碼模塊的形式化設(shè)計(jì)和驗(yàn)證研究[A];第二十一次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2006年

6 繆道期;;評(píng)審計(jì)算機(jī)安全等級(jí)[A];第二次計(jì)算機(jī)安全技術(shù)交流會(huì)論文集[C];1987年

7 趙曉峰;;城市軌道交通自主化信號(hào)系統(tǒng)全面創(chuàng)新實(shí)踐[A];中國(guó)系統(tǒng)工程學(xué)會(huì)第十八屆學(xué)術(shù)年會(huì)論文集——A12系統(tǒng)科學(xué)與系統(tǒng)工程理論在各個(gè)領(lǐng)域中的應(yīng)用研究[C];2014年

相關(guān)重要報(bào)紙文章 前1條

1 殷杰 安軍 山西大學(xué)科學(xué)技術(shù)哲學(xué)研究中心;21世紀(jì)科學(xué)哲學(xué)的關(guān)鍵詞:語(yǔ)境、科學(xué)理性與形式化[N];中國(guó)社會(huì)科學(xué)報(bào);2011年

相關(guān)博士學(xué)位論文 前8條

1 劉艷;互聯(lián)網(wǎng)內(nèi)容分級(jí)服務(wù)技術(shù)標(biāo)準(zhǔn)體系的形式化設(shè)計(jì)與驗(yàn)證[D];華中師范大學(xué);2015年

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

3 劉強(qiáng);設(shè)計(jì)模式的形式化研究及其EMF實(shí)現(xiàn)[D];華東師范大學(xué);2011年

4 張鵬;形式化方法在云計(jì)算中的應(yīng)用研究[D];吉林大學(xué);2014年

5 劉洋;網(wǎng)絡(luò)式軟件需求驗(yàn)證的形式化方法研究[D];電子科技大學(xué);2013年

6 王邁;語(yǔ)言形式化原理[D];上海外國(guó)語(yǔ)大學(xué);2011年

7 胡靜;基于Pi-演算的Web服務(wù)形式化描述模型[D];天津大學(xué);2013年

8 周寧;代數(shù)化符號(hào)模擬驗(yàn)證的應(yīng)用研究[D];北京交通大學(xué);2015年

相關(guān)碩士學(xué)位論文 前10條

1 王春曉;MDF連續(xù)平壓質(zhì)量控制形式化建模及優(yōu)化研究[D];東北林業(yè)大學(xué);2015年

2 王亞麗;面向機(jī)器人規(guī)劃的形式化研究[D];北京化工大學(xué);2015年

3 韓佳芮;基于Event-B和MAS的車(chē)站進(jìn)路聯(lián)鎖控制邏輯的形式化方法研究[D];蘭州交通大學(xué);2015年

4 徐世澤;基于Timed RAISE的RBC切換建模與分析[D];蘭州交通大學(xué);2015年

5 郭葉芳;電網(wǎng)控制系統(tǒng)軟件可靠性分析的形式化方法研究[D];華北電力大學(xué);2015年

6 黃峰;系統(tǒng)演化的形式化與具體化研究[D];南京郵電大學(xué);2014年

7 溫晉杰;Z規(guī)范對(duì)國(guó)產(chǎn)化軟件工程實(shí)踐的探討[D];石家莊鐵道大學(xué);2016年

8 丁寧;基于要素投影的事件本體形式化方法及其在情感分析中的應(yīng)用[D];上海大學(xué);2016年

9 沈崗;基于UML的形式化框架及其在安全協(xié)議驗(yàn)證中的應(yīng)用[D];天津大學(xué);2014年

10 Hamza I.Bangura;基于Z規(guī)格的軟件缺陷形式化方法[D];天津大學(xué);2010年

，

本文編號(hào)：1533612