微内核中断机制的形式化设计与验证

摘要：

操作系统的正确性和安全性很难用定量的方法进行描述.形式化方法是操作系统设计和验证领域公认的标准方法.以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证,在自行开发的安全可信操作系统VTOS上加以实现,采用Isabelle/HOL对设计过程进行了形式化描述,对VTOS中断机制的完整性进行了验证,这对操作系统的形式化设计和验证工作起到了一定的借鉴意义.

关键词：形式化设计、形式化验证、微内核、中断、完整性

所属期刊栏目：40

分类号：TP316(计算技术、计算机技术)

资助基金：国家高技术研究发展计划8632011AA01A202;江苏省"六大人才高峰"高层次人才项目2011-DZXX-035;江苏省高校自然科学研究项目12KJB520001

在线出版日期：2013-04-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：197-200,205