文件名称：px4vv:PX4 +模型检查
文件大小：16KB
文件格式：ZIP
更新时间：2024-06-14 13:18:45
C
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