软件学报

作者：金钊，金璐，张博闻，吴庆顺，冯朔，李冠峰，徐明亮

单位：金钊，郑州大学 计算机与人工智能学院, 河南 郑州 450001;智能集群系统教育部工程研究中心, 河南 郑州 450001;国家超级计算郑州中心, 河南 郑州 45000111,金璐，郑州大学 计算机与人工智能学院, 河南 郑州 45000102,张博闻，北京宇航系统工程研究所, 北京 10007603,吴庆顺，郑州大学 计算机与人工智能学院, 河南 郑州 45000104,冯朔，郑州大学 计算机与人工智能学院, 河南 郑州 450001;智能集群系统教育部工程研究中心, 河南 郑州 450001;国家超级计算郑州中心, 河南 郑州 45000105,李冠峰，中国船舶重工集团公司第七一三研究所, 河南 郑州 45001506,徐明亮，郑州大学 计算机与人工智能学院, 河南 郑州 450001;智能集群系统教育部工程研究中心, 河南 郑州 450001;国家超级计算郑州中心, 河南 郑州 45000107

关键词：舰载机弹药保障作业;形式化验证;分离逻辑;操作语义;Coq

基金：国家自然科学基金(62325602, 62302459, 62036010, 61972362, 62372416)

航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法, 是助推航母工程先进技术建设发展的重要途径之一. 高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈. 针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战, 基于分离逻辑的思想, 提出一种弹药保障系统的行为模型, 并利用定理证明器Coq对作业规划方案进行形式化验证. 首先提出一个符合弹药保障作业特征的序列化双层资源堆模型; 基于该模型, 构造一套可用于描述作业执行行为的建模语言及其操作语义; 最后在Coq中实现一种证明辅助工具. 通过几个典型弹药保障作业规划方案的交互式证明实例, 验证工具的可用性与工程实用性.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期