一种针对固件的半自动精化关系验证方法及系统

本发明涉及一种针对固件的半自动精化关系验证方法及系统，包括：S1、固件抽象规范层的形式验证：首先，对固件需求接口文档建模，进行属性规约即形式规约；接着，对属性规约使用一阶理论进行约束，生成抽象规范层的SMT表达式文件；S2、固件程序执行规范层的形式验证；S3、SMT‑LIB理论一致化：通过半自动化的方式，将SBI标准和程序行为均转换为SMT表达式，并对转换为SMT表达式的SBI标准和程序行为进行理论转换与语法统一；S4、SMT求解器形式验证：S5、生成验证报告：S6、验证报告可视化。本发明能够有效地验证固件是否满足需求规格，发现潜在的错误和安全漏洞。