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

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