近年来，在嵌入式安全关键领域，对软件系统安全性分析与验证已经成为软件工程研究领域中的一个热点问题。形式化方法是通过建立严格的数学模型来指导软件开发过程，并能增强人们对系统安全性的信心。形式化方法中，定理证明采用形式逻辑描述语言和相应的推理系统。与模型检测方法相比，其具有在证明过程中不受状态空间和相关输入约束的优点。针对嵌入式安全关键软件，操作表达式模型是目前定理证明中有效的形式化建模方法。本文采用操作表达式模型对一类典型的嵌入式软件（使用C语言安全子集Safety-C编写）展开安全性方面的程序证明，设计并实现了相关的原型工具。本文工作的主要研究内容包括以下4个部分：（1）针对安全关键软件的C语言安全子集，从数据类型、表达式以及程序控制三方面进行详细地特征分析；针对Safety-C软件系统，给出了C语言安全子集到操作表达式的转换规则与相应的转换流程；通过对操作表达式模型的预处理，并提出了模型分析树生成算法；（2）结合模型分析树的结构特点与操作表达式语义特性，给出分析树的节点语义谓词计算规则与相应的计算流程，构造出附有完整语义谓词的分析树；在消解原理与Coq定理证明器的辅助下，设计了基于语义谓词的分析树安全性验证框架，并给出验证执行引擎的设计结构，实现对系统形式规约的验证；（3）针对本文提出的面向C语言安全子集的软件安全性分析与验证方法，设计并实现相应的原型工具OESPA（Operation Expression Semantic PredicateAxioms），对OESPA的功能模块进行相应地说明，并给出该工具的设计框架与执行流程；（4）针对飞机襟缝翼控制软件系统进行实例分析，结合该系统的需求详细设计以及相关领域规范，利用原型工具对该系统的安全关键模块进行形式验证，给出相应的验证结果，并有效的说明本文提出的方法可行性与有效性。