系统软件是计算机系统的核心部分,其安全性和可靠性是构建高可信计算机系统的关键。而形式化验证技术基于严格的数学理论和方法,能够为系统软件的正确性提供强有力的保证。在系统软件中,内嵌汇编代码常被用于实现与底层硬件平台之间的交互。汇编代码的安全性和正确性对于保证整个系统的正确性是非常重要的。在某航天嵌入式操作系统的形式化验证工作项目中,该操作系统的内嵌汇编程序是由SPARCv8指令集编写的,而项目前期工作所采用的验证框架,无法验证这部分内嵌汇编程序的正确性。为了完善这一部分工作,本文基于己有的形式化验证技术提出了一套用于SPARCv8汇编程序验证的方法,并做出了如下贡献:首先,本文为SPARCv8汇编程序设计了一种霍尔风格的验证逻辑。并为验证逻辑中的推理规则提供了直接风格的(direct-style)、基于语义的解释。该验证逻辑支持SPARCv8汇编程序中函数调用的模块化验证,以及SPARCv8的三个特性的验证:包括延时跳转、特殊寄存器的延时写入和寄存器窗口机制。其次,应用所设计的验证逻辑,本文验证了某航天嵌入式操作系统中任务上下文切换程序的主要功能模块,累计共验证了约250行SPARCv8汇编程序代码。验证逻辑的定义,可靠性证明以及任务上下文切换程序的验证工作都在Coq辅助定理证明工具中实现。最后,本文提出了一种SPARCv8汇编程序与其所对应的抽象汇编原语之间的模拟关系,并证明了如果SPARCv8汇编程序与其所对应的汇编原语之间满足该模拟关系,那么他们之间满足上下文精化关系,即调用具体SPARCv8代码的程序,不会比调用抽象汇编原语的程序产生更多的行为。我们使用该方法证明了一个SPARCv8实现的任务上下文切换程序和任务调度原语switch之间满足该模拟关系。