一种基于模型检查的操作系统并发控制C代码验证系统及方法

本发明公开了一种基于模型检查的操作系统并发控制C代码验证系统及方法，涉及验证技术领域，该系统包括包括代码转换模块和验证模块；代码转换模块将目标操作系统并发控制C代码转换成BTOR2模型，再将BTOR2模型转换成AIGER模型；验证模块与代码转换模块连接，调用模型检查工具对AIGER模型进行验证，从而实现对操作系统并发控制C代码的验证，本发明通过模型转换工具链，将C代码逐步转换为BTOR2模型，再转换为AIGER模型，以兼容现有模型检查工具；替代传统定理证明方法，减少人工干预，提高验证效率，并能自动生成反例路径，精准定位系统缺陷；填补了多核操作系统代码使用模型检查方法验证的空白，拓展模型检查技术在软件领域的应用。