随着信息科学技术的逐渐成熟,嵌入式系统正在进入一个高速发展的全新时代。在航空航天、医疗设备、汽车电子等安全攸关领域中,嵌入式系统的安全可靠性和稳定性愈发重要。操作系统作为嵌入式系统的核心部分,负责管理软硬件组件并向用户提供各种服务,使整个系统实时高效率地运行。因此,如何保证操作系统的安全性和正确性是构建可信嵌入式系统的关键问题。形式化方法以其高度数学化和严谨性的特点,被广泛应用于系统可靠性分析工作中。然而,受验证工具的限制以及操作系统自身特点的影响,形式化方法在操作系统验证中的应用仍面临许多挑战。例如,自动化验证工具的灵活性有一定局限性,很难建立在一定领域中通用的模型来分析操作系统的各个组成部分。另外,操作系统内核通常使用高级语言和汇编指令混合实现,为了统一高级与汇编程序的抽象模型,目前大多数方法是抽象汇编程序,或向下编译高级语言程序,然后反汇编并在统一的汇编程序上建立模型,而很难实现对原始代码程序的验证。本文基于操作系统验证工作中存在的挑战,结合重写逻辑理论的最新建模方法,以汽车电子操作系统为研究对象,对嵌入式操作系统的建模和验证技术进行了研究,建立了汽车电子操作系统规范以及内核实现的语义模型,在语义模型的基础上分别对操作系统规范、内核和应用的正确性进行了分析和验证。具体的,本文主要研究内容和贡献如下:·建立了完整的车载操作系统OSEK规范的语义模型。OSEK规范的语义模型定义了操作系统任务调度、资源管理、事件管理、错误处理、中断机制和报警机制相关的系统服务执行规则,并刻画了系统服务和应用程序的执行时间。对于自然语言规范中未定义或有二义性的行为进行了重定义,应用可达性检查方法分析了重定义行为的合理性。·提出了面向嵌入式操作系统内核的混合语言程序分析方法。定义了操作系统内核中抽象的汇编指令、C语言子集以及其混合语言的操作语义,语义规则覆盖了不同语言间子程序调用以及共享变量的执行情况。基于混合语言的操作语义,应用可达性逻辑证明系统可证明混合语言程序的可达性。结合基于重写逻辑理论的分析工具,自动化验证了内核中上下文切换程序的原子执行性。·实现了操作系统规范、内核和应用的自动化验证。基于完整的OSEK规范模型,分别验证了规范中任务调度、事件管理、资源管理和报警机制的正确性。对规范模型的验证,一方面为确定规范中未定义行为的执行规则提供了参考意义,另一方面可分析操作系统性质,减小系统层性质分析的验证代价。另外,基于内核和规范的语义模型,分别对普华基础软件公司所开发的OSEK操作系统内核与应用程序的代码进行验证,并发现了应用程序中潜在的缺陷,展现了本文方法的实用性。