一种针对嵌入式实时操作系统形式化验证方法，采用分阶段的思路对嵌入式实时操作系统进行形式化验证，首先按照需求、设计、实现三个阶段进行形式化建模和验证，用具有严格数学定义的语法、语义的语言来描述操作系统，然后建立操作系统的形式化模型，提取待验证的性质，通过数学方法分析及验证形式化模型是否满足期望的性质，通过反复迭代，最终得到满足期望性质的形式化模型。本发明方法与现有技术相比，解决了传统测试方法对无法保证操作系统需求的正确性以及代码和需求一致性的问题，具有较好的使用价值。