摘要
航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器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.
作者
金钊
金璐
张博闻
吴庆顺
冯朔
李冠峰
徐明亮
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)
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4100-4122,共23页
Journal of Software
基金
国家自然科学基金(62325602,62302459,62036010,61972362,62372416)。
关键词
舰载机弹药保障作业
形式化验证
分离逻辑
操作语义
COQ
carrier-borne aircraft ammunition support operation
formal verification
separation logic
operational semantics
Coq
