本文關(guān)鍵詞：操作系統(tǒng)匯編級形式化設(shè)計和驗證方法

  更多相關(guān)文章： 操作系統(tǒng) 正確性驗證 形式化方法 系統(tǒng)狀態(tài)模型

【摘要】：由于系統(tǒng)的巨大規(guī)模,操作系統(tǒng)設(shè)計和實現(xiàn)的正確性很難用傳統(tǒng)的方法進行描述和驗證.在匯編層形式化地對系統(tǒng)模塊的功能語義進行建模,提出一種匯編級的系統(tǒng)狀態(tài)模型,作為匯編語言層設(shè)計和驗證的紐帶.通過定義系統(tǒng)狀態(tài)模型的合法狀態(tài)和狀態(tài)轉(zhuǎn)換函數(shù)來建立系統(tǒng)狀態(tài)模型的論域,并以此來描述匯編層的論域.通過驗證匯編層的功能模塊的正確性來保證匯編語言層設(shè)計的正確性,達到對系統(tǒng)功能實現(xiàn)的正確性驗證.同時,使用定理證明工具Isabelle/HOL來形式化地描述這一系統(tǒng)狀態(tài)模型,基于這一形式化模型,在Isabelle/HOL中驗證系統(tǒng)模塊的功能語義的正確性.以實現(xiàn)的安全可信OS(verified secure operating system,簡稱VSOS)為例,闡述了所提出的形式化設(shè)計和驗證方法,說明了這一方法的可行性.
【作者單位】： 南京大學計算機科學與技術(shù)系;常熟理工學院計算機科學與工程學院;King’s
【關(guān)鍵詞】： 操作系統(tǒng) 正確性驗證 形式化方法 系統(tǒng)狀態(tài)模型
【基金】：國家自然科學基金(61402057) 江蘇省科技計劃自然科學研究項目(BK20140418) 中國博士后科學基金(2015M571737) 江蘇省“六大人才高峰”高層次人才項目(2011-DZXX-035) 江蘇省高校自然科學研究項目(12KJB520001)~~
【分類號】：TP316
【正文快照】： 3(King’s College London,London WC2R 2LS,UK)www.jos.org.cn/1000-9825/4851.htm英文引用格式:Qian ZJ,Huang H,Song FM.Method of formal design and verification of OS on assembly layer.Ruan Jian XueBao/Journal of Software,2016,27(12):3143?3157(in Chinese).http

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 姜利;孫永強;;形式化方法的發(fā)展及展望[J];計算機科學;1998年02期

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

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

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

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

6 ;《軟件學報》形式化方法和工具專刊征文通知[J];軟件學報;2010年07期

7 王戟;李宣東;;形式化方法與工具專刊前言[J];軟件學報;2011年06期

8 胡家寶，，姚干洲;形式化方法的回顧（續(xù)一）[J];計算機與現(xiàn)代化;1994年04期

9 鄭紅軍;張乃孝;;軟件開發(fā)中的形式化方法[J];計算機科學;1997年06期

10 柴振榮;形式化方法與軟件的可靠性[J];管理科學文摘;1999年09期

中國重要會議論文全文數(shù)據(jù)庫 前4條

1 鄭宇軍;石海鶴;薛錦云;;Spec#語言中的形式化特性[A];2005年全國理論計算機科學學術(shù)年會論文集[C];2005年

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

3 苗潔君;王克;;密碼模塊的形式化設(shè)計和驗證研究[A];第二十一次全國計算機安全學術(shù)交流會論文集[C];2006年

4 繆道期;;評審計算機安全等級[A];第二次計算機安全技術(shù)交流會論文集[C];1987年

中國博士學位論文全文數(shù)據(jù)庫 前4條

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

2 劉強;設(shè)計模式的形式化研究及其EMF實現(xiàn)[D];華東師范大學;2011年

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

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

中國碩士學位論文全文數(shù)據(jù)庫 前10條

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

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

3 鐘琪;軟件分析模式的形式化研究[D];西南師范大學;2004年

4 郭忠偉;神經(jīng)內(nèi)分泌復雜系統(tǒng)的形式化研究[D];揚州大學;2009年

5 王曉帆;基于模糊數(shù)學的形式化開發(fā)方法研究[D];西安理工大學;2003年

6 閔洪軍;軟件工程中形式化方法研究[D];浙江大學;2006年

7 張楊;UML模型形式化轉(zhuǎn)換及驗證的研究[D];太原理工大學;2013年

8 匡春臨;并發(fā)系統(tǒng)的形式化技術(shù)研究[D];華僑大學;2008年

9 白銳;ATP系統(tǒng)形式化開發(fā)方法的研究[D];蘭州交通大學;2014年

10 解方;從UML建模到Z形式化規(guī)范的研究[D];太原理工大學;2013年

本文編號：819915