嵌入式操作系统的形式化验证研究

摘要：

描述了一个汽车电子嵌入式实时操作系统的分层形式模型:在低层,该操作系统的顺序内核承担基础设施的角色,实施任务、ISR和系统服务等并发执行体之间的切换;而在高层,该操作系统向用户提供可并发执行的系统服务.两个层次的模型具有不同的配置状态视图和操作粒度.作为最重要的安全相关特性,应用与OS之间的存储隔离保护机制在顺序内核的模型中得以体现.建立了操作系统的实现正确性定理,包括相应的仿真关系和实现不变量.根据该操作系统两个部分模型的特点及相应代码的实现语言情况,选择组合应用定理证明器Isabelle/HOL和程序验证工具VCC的方式,有效完成了该操作系统的形式化验证.

关键词：嵌入式操作系统、形式化验证、建模、Isabelle/HOL、VCC

所属期刊栏目：42

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

资助基金：国家自然科学基金项目61401067;四川省应用基础研究项目2013JY0002

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

页数：共12页

页码：203-214