px4vv:PX4 +模型检查

PX4验证和验证版本 这是用于平台独立px4兼容自动驾驶仪的原型代码库，该自动驾驶仪已通过CBMC模型检查器进行了验证。 请注意，CBMC使用C语言而不是C ++更为简单，所以现在我要用C手动重写代码块。 这可能会导致使用C语言编写的新代码库，或者将此处开发的某些功能作为当前模块的V＆V版本拉回到使用C和C ++语言编写的主代码库中。 安装 ###依赖关系： 中央银行 为Linux安装的示例依赖项： sudo apt-get install cmake cbmc mkdir build cd build cmake .. make 例子 转换规则以易于阅读的形式写在源代码中，例如： enum { // table columns T_STATE = 0 , // current vehicle state T_REQUEST, // requested vehicle st