舰载机弹药保障作业调度的形式化建模与验证  

Formal Modeling and Verification of Carrier-borne Aircraft Ammunition Support Operation Scheduling

作　　者：金钊 金璐[1] 张博闻 吴庆顺 冯朔 李冠峰[5] 徐明亮[1,2,3] JIN Zhao;JIN Lu;ZHANG Bo-Wen;WU Qing-Shun;FENG Shuo;LI Guan-Feng;XU Ming-Liang(School of Computer and Artificial Intelligence,Zhengzhou University,Zhengzhou 450001,China;Engineering Research Center of Intelligent Swarm Systems,Ministry of Education,Zhengzhou 450001,China;National Supercomputing Center in Zhengzhou,Zhengzhou 450001,China;Beijing Institute of Astronautical Systems Engineering,Beijing 100076,China;The 713 Research Institute of China Shipbuilding Industry Corporation,Zhengzhou 450015,China)

机构地区：[1]郑州大学计算机与人工智能学院,河南郑州450001 [2]智能集群系统教育部工程研究中心,河南郑州450001 [3]国家超级计算郑州中心,河南郑州450001 [4]北京宇航系统工程研究所,北京100076 [5]中国船舶重工集团公司第七一三研究所,河南郑州450015

出　　处：《软件学报》2024年第9期4100-4122,共23页Journal of Software

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

摘　　要：航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器Coq对作业规划方案进行形式化验证.首先提出一个符合弹药保障作业特征的序列化双层资源堆模型;基于该模型,构造一套可用于描述作业执行行为的建模语言及其操作语义;最后在Coq中实现一种证明辅助工具.通过几个典型弹药保障作业规划方案的交互式证明实例,验证工具的可用性与工程实用性.As an efficient scheduling method,the intelligent planning of ammunition support operation of carrier-borne air craft is an important way to boost the development of advanced technology of aircraft carrier engineering.Ensuring the correctness of operation planning schemes under the high safety-critical attribute has gradually become the key technical bottleneck restricting the security of their practical application deployments.Aiming at the challenges posed by the difficulties in modeling ammunition support systems,describing operation execution behavior,and realizing formal verification tools,this study proposes a behavior model for ammunition support systems based on the separation logic idea,where the theorem prover Coq is employed to conduct formal verification on the operation planning scheme.First,a serialized two-tier resource heap model that conforms to the characteristics of ammunition support operation is proposed.Subsequently,a set of modeling language and operational semantics are constructed based on this model to describe job execution behavior.Finally,a proof assistant tool is implemented in Coq.The usability and engineering practicability of the tool are verified by interactive demonstrations of several typical ammunition support operation planning schemes.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]