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

• 作者: 李康杰 钱振江 黄皓
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 形式化设计 形式化验证 微内核 中断 完整性
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 信息安全
• 页码范围: 197-200,205
• 页数: 5页
• 分类号: TP316
• 字数: 4411字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学软件新技术国家重点实验室	140	1805	24.0	35.0
5	钱振江	南京大学软件新技术国家重点实验室	16	90	6.0	8.0
9	李康杰	南京大学软件新技术国家重点实验室	1	6	1.0	1.0