一种群体智能操作系统的形式化验证方法及装置

摘要

本发明公开了一种群体智能操作系统的形式化验证方法及装置，该方法在Isabelle环境下执行，该方法采用Isabelle元语言构造需求层形式化模型包括：对ROS数据结构、ROS接口、ROS日志输出库进行抽象建模；其中，对ROS数据结构进行抽象建模包括：构建ROS节点形式化模型和句柄形式化模型；对ROS接口进行抽象建模包括：对初始化函数、日志输出函数、获取函数、服务绑定函数、服务调用函数进行接口描述；对ROS日志输出库进行抽象建模包括：使用Show方法对将程序的状态或变量转换为字符串输出的操作进行描述。本发明能够保证安全需求在实现阶段得到满足，经过验证的操作系统可以达到CC认证标准。