计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
3期
197-200,205
,共5页
形式化设计%形式化验证%微内核%中断%完整性
形式化設計%形式化驗證%微內覈%中斷%完整性
형식화설계%형식화험증%미내핵%중단%완정성
操作系统的正确性和安全性很难用定量的方法进行描述.形式化方法是操作系统设计和验证领域公认的标准方法.以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证,在自行开发的安全可信操作系统VTOS上加以实现,采用Isabelle/HOL对设计过程进行了形式化描述,对VTOS中断机制的完整性进行了验证,这对操作系统的形式化设计和验证工作起到了一定的借鉴意义.
操作繫統的正確性和安全性很難用定量的方法進行描述.形式化方法是操作繫統設計和驗證領域公認的標準方法.以操作繫統對象語義模型(OSOSM)為基礎,採用形式化方法對微內覈架構的中斷機製進行瞭設計和驗證,在自行開髮的安全可信操作繫統VTOS上加以實現,採用Isabelle/HOL對設計過程進行瞭形式化描述,對VTOS中斷機製的完整性進行瞭驗證,這對操作繫統的形式化設計和驗證工作起到瞭一定的藉鑒意義.
조작계통적정학성화안전성흔난용정량적방법진행묘술.형식화방법시조작계통설계화험증영역공인적표준방법.이조작계통대상어의모형(OSOSM)위기출,채용형식화방법대미내핵가구적중단궤제진행료설계화험증,재자행개발적안전가신조작계통VTOS상가이실현,채용Isabelle/HOL대설계과정진행료형식화묘술,대VTOS중단궤제적완정성진행료험증,저대조작계통적형식화설계화험증공작기도료일정적차감의의.
