首页 | 官方网站   微博 | 高级检索  
     

微内核中断机制的形式化设计与验证
引用本文:李康杰,钱振江,黄皓.微内核中断机制的形式化设计与验证[J].计算机科学,2013,40(3):197-200.
作者姓名:李康杰  钱振江  黄皓
作者单位:(南京大学软件新技术国家重点实验室 南京 210046)(南京大学计算机科学与技术系 南京 210046)
摘    要:操作系统的正确性和安全性很难用定量的方法进行描述。形式化方法是操作系统设计和验证领域公认的标 准方法。以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证, 在自行开发的安全可信操作系统VTOS上加以实现,采用Isabelle/HOL对设计过程进行了形式化描述,对VTOS中 断机制的完整性进行了验证,这对操作系统的形式化设计和验证工作起到了一定的借鉴意义。

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

Formal Design and Verification of Interrupt Mechanism Based on Microkernel
Abstract:It is difficult to describe the correctness and security of the operate system (OS) by quantitative analysis. Formal method is the acknowledged standard one in design and verification for OS. Based on the operate system object semantics model (OSOSM) , we designed and verified the interruption mechanism of microkernel architecture using for- mal method,which was realized on our self-implemented verified trusted operate system (VTOS). Meanwhile,we used the theorem prover Isabelle/HOI. to formally describe the design process, and verify the integrality of the interruption mechanism of VTOS. Our research plays certain referential significance on formal design and verification of OS.
Keywords:Formal design  Formal verification  Microkernel  Interrupt  Integrity
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司    京ICP备09084417号-23

京公网安备 11010802026262号