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