微信服务号

微信订阅号

2025-4-8- 4
Home > Archive>Volume 35, Issue 9, 2024 >4100-4122. DOI:10.13328/j.cnki.jos.007128
PDF HTML XML Export Cite reminder
Formal Modeling and Verification of Carrier-borne Aircraft Ammunition Support Operation Scheduling
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [47]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    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.

    Reference
    [1] 李亚飞, 吴庆顺, 徐明亮, 吕培, 姜晓恒, 朱睿杰, 周兵. 基于强化学习的舰载机保障作业实时调度方法. 中国科学: 信息科学, 2021, 51(2): 247–262.
    Li YF, Wu QS, Xu ML, Lv P, Jiang XH, Zhu RJ, Zhou B. Real-time scheduling for carrier-borne aircraft support operations: A reinforcement learning approach. Scientia Sinica Informationis, 2021, 51(2): 247–262 (in Chinese with English abstract).
    [2] 张磊, 高鹏, 杜志鹏, 刘海燕, 王健. 基于航空保障能力定量分析的航母毁伤评估判据研究. 舰船科学技术, 2022, 44(11): 185–189.
    Zhang L, Gao P, Du ZP, Liu HY, Wang J. Research on aircraft carrier damage evaluation criteria based on quantitative analysis of aviation support capability. Ship Science and Technology, 2022, 44(11): 185–189 (in Chinese with English abstract).
    [3] 肖虎斌. 航母弹药贮运安全作业研究. 飞航导弹, 2019(4): 85–88, 95.
    Xiao HB. Research on the safety of ammunition stowage and handling aboard aircraft carriers. Aerodynamic Missile Journal, 2019(4): 85–88, 95 (in Chinese).
    [4] 田德红, 何建敏, 齐洁, 孙海信. 航空弹药动态调运决策优化建模与仿真研究. 西北工业大学学报, 2018, 36(6): 1236–1242.
    Tian DH, He JM, Qi J, Sun HX. Research on the modeling and simulation of optimal dynamic aerial ammunition scheduling and transportation. Journal of Northwestern Polytechnical University, 2018, 36(6): 1236–1242 (in Chinese with English abstract).
    [5] 刘翱, 刘克. 舰载机保障作业调度问题研究进展. 系统工程理论与实践, 2017, 37(1): 49–60.
    Liu A, Liu K. Advances in carrier-based aircraft deck operation scheduling. Systems Engineering-theory & Practice, 2017, 37(1): 49–60 (in Chinese with English abstract).
    [6] 陶俊权, 苏析超, 韩维, 李亚飞. 基于EDA算法的航母弹药调度优化研究. 兵器装备工程学报, 2022, 43(5): 125–131.
    Tao JQ, Su XC, Han W, Li YF. Study of aircraft carrier ammunition scheduling optimization based on EDA algorithm. Journal of Ordnance Equipment Engineering, 2022, 43(5): 125–131 (in Chinese with English abstract).
    [7] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm
    Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm
    [8] 王淑灵, 詹博华, 盛欢欢, 吴昊, 易士程, 王令泰, 金翔宇, 薛白, 李静辉, 向霜晴, 向展, 毛碧飞. 可信系统性质的分类和形式化研究综述. 软件学报, 2022, 33(7): 2367–2410. http://www.jos.org.cn/1000-9825/6587.htm
    Wang SL, Zhan BH, Sheng HH, Wu H, Yi SC, Wang LT, Jin XY, Xue B, Li JH, Xiang SQ, Xiang Z, Mao BF. Survey on requirements classification and formalization of trustworthy systems. Ruan Jian Xue Bao/Journal of Software, 2022, 33(7): 2367–2410 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6587.htm
    [9] 詹乃军, 王戟. 复杂系统规约、分析与验证发展现状与展望. 前瞻科技, 2023, 2(1): 7–22. [doi: 10.3981/j.issn.2097-0781.2023.01.001]
    Zhan NJ, Wang J. Challenges and trends for specification, analysis, and verification of complex systems. Science and Technology Foresight, 2023, 2(1): 7–22 (in Chinese with English abstract).
    [10] Reynolds JC. Separation Logic: A logic for shared mutable data structures. In: Proc. of the 17th IEEE Symp. on Logic in Computer Science. Copenhagen: IEEE, 2002. 55–74. [doi: 10.1109/LICS.2002.1029817]
    [11] Pym D, Spring JM, O’Hearn PW. Why separation logic works. Philosophy & Technology, 2019, 32(3): 483–516.
    [12] O’Hearn PW. Separation logic. Communications of the ACM, 2019, 62(2): 86–95.
    [13] Chen HG, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N. Using Crash Hoare logic for certifying the FSCQ file system. In: Proc. of the 25th Symp. on Operating Systems Principles. Monterey: Association for Computing Machinery, 2015. 18–37.
    [14] Xu FW, Fu M, Feng XY, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernel. In: Proc. of the 28th Int’l Conf. on Computer Aided Verification. Toronto: Springer, 2016. 57–59. [doi: 10.1007/978-3-319-41540-6_4]
    [15] Amani S, Bégel M, Bortin M, Staples M. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: Proc. of the 7th ACM SIGPLAN Int’l Conf. on Certified Programs and Proofs. Los Angeles: Association for Computing Machinery, 2018. 66–77.
    [16] Le QL, Raad A, Villard J, Berdine J, Dreyer D, O’Hearn PW. Finding real bugs in big programs with incorrectness logic. Proc. of the ACM on Programming Languages, 2022, 6: 81.
    [17] Distefano D, F?hndrich M, Logozzo F, O’Hearn PW. Scaling static analyses at Facebook. Communications of the ACM, 2019, 62(8): 62–70.
    [18] Cao QX, Beringer L, Gruetter S, Dodds J, Appel AW. VST-Floyd: A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 2018, 61(1): 367–422.
    [19] Feng XY, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. ACM SIGPLAN Notices, 2008, 43(6): 170–182.
    [20] Zhan BH. AUTO2, a saturation-based heuristic prover for higher-order logic. In: Proc. of the 7th Int’l Conf. on Interactive Theorem Proving. Nancy: Springer, 2016. 441–456. [doi: 10.1007/978-3-319-43144-4_27]
    [21] 章乐平, 赵永望, 王布阳, 李悦欣, 冯潇潇. L4虚拟内存子系统的形式化验证. 软件学报, 2022, 34(8): 3527–3548. http://www.jos.org.cn/1000-9825/6869.htm
    Zhang LP, Zhao YW, Wang BY, Li YX, Feng XX. Formal verification of virtual memory subsystem in L4. Ruan Jian Xue Bao/Journal of Software, 2023, 34(8): 3527–3548 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6869.htm
    [22] 王小兵, 寇蒙莎, 李春奕, 赵亮. 支持索引式的PPTL定理证明器的实现. 软件学报, 2022, 33(6): 2172–2188. http://www.jos.org.cn/1000-9825/6576.htm
    Wang XB, Kou MS, Li CY, Zhao L. Implementation of theorem prover for PPTL with indexed expressions. Ruan Jian Xue Bao/Journal of Software, 2022, 33(6): 2172–2188 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6576.htm
    [23] 李亚男, 邓玉欣, 刘静. 基于Coq的Paxos形式化建模与验证. 软件学报, 2020, 31(8): 2362–2374. http://www.jos.org.cn/1000-9825/5960.htm
    Li YN, Deng YX, Liu J. Formal modeling and verification of Paxos based on Coq. Ruan Jian Xue Bao/Journal of Software, 2020, 31(8): 2362–2374 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5960.htm
    [24] 苏婉昀, 高冲, 古新才, 吴志林. COMPSPEN: 对形状性质与数据约束进行融合推理的分离逻辑求解器. 软件学报, 2023, 34(5): 2181–2195. http://www.jos.org.cn/1000-9825/6407.htm
    Su WY, Gao C, Gu XC, Wu ZL. COMPSPEN: Separation logic solver for integrated reasoning about shape properties and data constraints. Ruan Jian Xue Bao/Journal of Software, 2023, 34(5): 2181–2195 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6407.htm
    [25] 张博闻, 金钊, 王捍贫, 曹永知. 一种基于分离逻辑的块云存储系统验证工具. 软件学报, 2022, 33(6): 2264–2287. http://www.jos.org.cn/1000-9825/6581.htm
    Zhang BW, Jin Z, Wang HP, Cao YZ. Tool for verifying cloud block storage based on separation logic. Ruan Jian Xue Bao/Journal of Software, 2022, 33(6): 2264–2287 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6581.htm
    [26] Liu YJ, Han W, Su XC, Cui RW. Optimization of fixed aviation support resource station configuration for aircraft carrier based on aircraft dispatch mission scheduling. Chinese Journal of Aeronautics, 2023, 36(2): 127–138.
    [27] Jin Z, Zhang BW, Cao TY, Cao YZ, Wang HP. Reasoning about block-based cloud storage systems via separation logic. Theoretical Computer Science, 2022, 936: 43–76.
    [28] 张少辉, 刘舜, 李亚飞, 金钊, 靳远远, 王少参, 赵建波, 徐明亮. 航空母舰舰载机弹药保障作业调度优化算法. 航空学报, 2023, 44(20): 228485.
    Zhang SH, Liu S, Li YF, Jin Z, Jin YY, Wang SC, Zhao JB, Xu ML. Optimization algorithm for ammunition support operation scheduling of carrier-borne aircraft. Acta Aeronautica et Astronautica Sinica, 2023, 44(20): 228485 (in Chinese with English abstract).
    [29] 李冠峰. 弹药安全上舰设计分析. 舰船科学技术, 2022, 44(2): 166–169.
    Li GF. Design analysis about ammunition boarding safely. Ship Science and Technology, 2022, 44(2): 166–169 (in Chinese with English abstract).
    [30] 李亚飞, 高磊, 蒿宏杰, 靳远远, 王可, 徐明亮. 舰载机保障作业人机协同决策方法. 中国科学: 信息科学, 2023, 53(12): 2493–2510.
    Li YF, Gao L, Hao HJ, Jin YY, Wang K, Xu ML. Human-machine collaborative decision-making for carrier aircraft support operations. Scientia Sinica Informationis, 2023, 53(12): 2493–2510 (in Chinese with English abstract).
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

金钊,金璐,张博闻,吴庆顺,冯朔,李冠峰,徐明亮.舰载机弹药保障作业调度的形式化建模与验证.软件学报,2024,35(9):4100-4122

Copy
Share
Article Metrics
  • Abstract:744
  • PDF: 3125
  • HTML: 1069
  • Cited by: 0
History
  • Received:September 11,2023
  • Revised:October 30,2023
  • Online: January 05,2024
  • Published: September 06,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033794Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063