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

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

Modeling and Verification of Carrier-Borne Aircraft Ammunition Support Operation Scheduling

An important way of boosting the development of advanced technology of aircraft carrier engineering is the intelligent planning of ammunition support operation of carrier aircraft, as an efficient scheduling method. 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 presented by the difficulties in modeling ammunition support systems, describing operation execution behavior, and realizing formal verification tools, a behavior model is proposed for ammunition support systems based on the idea of separation logic, whereby the theorem prover Coq is used to formalize 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 through interactive demonstrations of several typical ammunition support operation planning schemes.