| 舰载机弹药保障作业调度的形式化建模与验证 |
| |
| 作者姓名： | 金钊 金璐 张博闻 吴庆顺 冯朔 李冠峰 徐明亮 |
| |
| 作者单位： | 郑州大学 计算机与人工智能学院, 河南 郑州 450001;智能集群系统教育部工程研究中心, 河南 郑州 450001;国家超级计算郑州中心, 河南 郑州 450001;北京宇航系统工程研究所, 北京 100076;中国船舶重工集团公司第七一三研究所, 河南 郑州 450015 |
| |
| 基金项目： | 国家自然科学基金重点项目(62036010);国家自然科学基金杰出青年基金(62325602);国家自然科学基金青年科学基金(62302459);国家自然科学基金面上项目(61972362,62372416) |
| |
| 摘 要： | 
航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战,基于分离逻辑的思想,提出一种弹药保障系统的行为模型,并利用定理证明器Coq对作业规划方案进行形式化验证.
首先提出一个符合弹药保障作业特征的序列化双层资源堆模型;基于该模型,构造一套可用于描述作业执行行为的建模语言及其操作语义;最后在Coq中实现一种证明辅助工具.通过几个典型弹药保障作业规划方案的交互式证明实例,验证工具的可用性与工程实用性.
|
| 关 键 词： | 舰载机弹药保障作业 形式化验证 分离逻辑 操作语义 Coq |
| 收稿时间： | 2023-09-11 |
| 修稿时间： | 2023-10-30 |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载免费的PDF全文 |
|
