-
题名舰载机弹药保障作业调度的形式化建模与验证
- 1
-
-
作者
金钊
金璐
张博闻
吴庆顺
冯朔
李冠峰
徐明亮
-
机构
郑州大学计算机与人工智能学院
智能集群系统教育部工程研究中心
国家超级计算郑州中心
北京宇航系统工程研究所
中国船舶重工集团公司第七一三研究所
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4100-4122,共23页
-
基金
国家自然科学基金(62325602,62302459,62036010,61972362,62372416)。
-
文摘
航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器Coq对作业规划方案进行形式化验证.首先提出一个符合弹药保障作业特征的序列化双层资源堆模型;基于该模型,构造一套可用于描述作业执行行为的建模语言及其操作语义;最后在Coq中实现一种证明辅助工具.通过几个典型弹药保障作业规划方案的交互式证明实例,验证工具的可用性与工程实用性.
-
关键词
舰载机弹药保障作业
形式化验证
分离逻辑
操作语义
COQ
-
Keywords
carrier-borne aircraft ammunition support operation
formal verification
separation logic
operational semantics
Coq
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
