汽车电控部件的软件正确性验证系统及其验证方法

摘要

本发明提供一种汽车电控部件的软件正确性验证系统，包括规范定义模块，对汽车电控部件功能进行数学化定义，生成形式化规范；软件功能验证模块，利用数学定理自动证明算法，检测汽车电控部件控制软件是否满足规范定义模块生成的形式化规范。本发明还提供一种汽车电控部件的软件正确性验证系统的验证方法，将具有高可信的形式化验证应用于汽车系统的验证中，从而使汽车系统的安全性能得到更大的保障。