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

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

基于改进遗传算法的舰载机弹药挂载调度

舰载机弹药挂载工作是舰载机弹药保障中的一个重要环节,传统的舰载机弹药挂载调度通常忽略工作中存在的约束。针对该问题,分析了弹药挂载工作中存在的约束条件,以所有舰载机弹药挂载时间之和为优化目标,建立了考虑舰载机起始挂载时间不同和弹药挂载空间约束的舰载机弹药挂载调度模型,并提出了一种基于染色体片段编码的改进遗传算法,避免了大量不可行解的产生,提高了算法求解效率。仿真分析验证了所提模型与算法所得弹药挂载调度方案的可行性。

舰载机模块化弹药调度方案优化设计

舰载机模块化弹药存储和调度是未来发展的主要趋势之一。模块化弹药调度与整弹调度相比,调度对象的数量成倍增加并且多了一个弹药装配环节,使调度工作的难度呈指数级增长。针对模块化弹药调度问题,建立以任务完成时间最小化和各舱室与升降机平均工作时间最小化为优化目标,以各模块调度次序、机器选择和调度起始时间为约束条件的舰载机模块化弹药调度模型,设计递推法计算任务完成时间,并使用改进的遗传算法对模型进行求解,结合模块化弹药特点优化多层编码方式,使染色体更加完整地表达弹药在各个阶段的信息。通过仿真验证,所提的舰载机模块化弹药调度方法生成的调度方案具有可行性。