微信服务号

微信订阅号

2025年5月1日 17:24 星期四
首页 > 过刊浏览>2022年第33卷第6期 >2150-2171. DOI:10.13328/j.cnki.jos.006575
PDF HTML阅读 XML下载 导出引用 引用提醒
多旋翼飞控推进子系统的Coq形式化验证
作者:
作者简介:

石正璞(1986-),男,博士生,CCF学生会员,主要研究领域为形式化工程数学,Coq定理证明,飞行控制系统,硬件设计,嵌入式系统;谢果君(1992-),男,博士生,CCF学生会员,主要研究领域为形式化工程数学,控制系统形式化,定理证明;陈钢(1958-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为形式化工程数学,COQ定理证明,函数式语言,类型系统,形式化方法,控制系统

通讯作者:

陈钢,E-mail:gangchensh@qq.com

中图分类号:

TP311


Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [30]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

    Abstract:

    A highly reliable flight control system (FCS) is a necessary prerequisite for the reliable operation of an aircraft. Under the traditional development approach, the domain knowledge is first modeled by the human in the form of natural language, and then code is written by humans according to the model, and finally, the software defects are eliminated by using testing technology. The approach fails to build reliable FCS, because of human error, natural language ambiguity, and incompleteness of test techniques. A novel development approach based on formal verification technology could improve the reliability of FCS from many aspects. This paper presents a formal design and verification method for multicopter propulsion subsystem based on Coq and generated a usable and highly reliable functional software library. The main work of this study includes:the domain knowledge is organized into a hierarchical document suitable for formal verification, the basic functions, and composite functions are separated, and the concept of the simplest form of function (SFF) is proposed; formalize the system in Coq according to this document, defining constants, variables, basic functions, composite functions, SFF, axioms, etc.; the correctness of the derivation of all kinds of composite functions is expressed as lemmas and be proved; the algorithm for solving practical problems such as the longest hover time of multicopter is given; and a functional software library is generated using OCaml language by COQ program extraction ability. In the future, more subsystems of FCS will be developed based on formal verification, and finally, a complete and highly reliable FCS with formal verification will be established.

    参考文献
    [1] Quan Q. Introduction to Multicopter Design and Control. Springer, 2017.[doi:10.1017/aer.2018.133]
    [2] Quan Q. Introduction to Multicopter Design and Control. Beijing:Publishing House of Electronics Industry, 2018(in Chinese).
    [3] Phillip J, Harris R. The Boeing 737 MAX Saga:Lessons for software organizations. Software Quality Professional, 2019, 21(3):4-12.
    [4] Ducard GJJ. Fault-tolerant flight control and guidance systems for a small unmanned aerial vehicle. ETH Zurich, 2007.[doi:10. 3929/ETHZ-A-005582839]
    [5] Xu M. The Basis of Air and Gas Dynamics. 2nd ed., Northwestern Polytechnical University Press Co. Ltd., 2015(in Chinese).
    [6] 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/10000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [7] Chen G, Shi ZP. Formalized engineering mathematics. Communications of the CCF, 2017, 13(10)(in Chinese with English abstract).
    [8] Chen G Formalized mathematics and proof engineering. Communications of the CCF, 2016, 12(9)(in Chinese with English abstract).
    [9] Fisher K, Launchbury J, Richards R. The HACMS program:USIng formal methods to eliminate exploitable bugs. Philosophical Trans. of the Royal Society A, 2017, 375:20150401.[doi:10.1098/rsta.2015.0401]
    [10] Shi D, Dai X. A practical performance evaluation method for electric multicopters. IEEE/ASME Trans. on Mechatronics, 2017, 22(3):1337-1348.[doi:10.1109/TMECH.2017.2675913]
    [11] Boldo S, Lelay C, Melquiond G. Coquelicot:A user-friendly library of real analysis for Coq. Mathematics Computer Science, 2015, 9(1):41-62.[doi:10.1007/s11786-014-0181-1]
    [12] Mathematical Components. https://math-comp.github.io[doi:10.5281/zenodo.4457887]
    [13] Abed S, Rashid A, Hasan O. Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving. Journal of Aerospace Information Systems, 2020, 17(9):481-495.[doi:10.2514/1.I010730]
    [14] Vermaelen H, Dinh T, Holvoet T. Formal verification of autonomous UAV behavior for inspection tasks using the knowledge base system IDP. In:Demazeau Y, Holvoet T, Corchado JM, Costantini S, eds., Advances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection, Vol.12092. Cham:Springer International Publishing, 2020. 315-326.[doi:10.1007/978-3-030-49778-1_25]
    [15] Pollien B, Garion C, Hattenberger G, Roux P, Thirioux X. Verifying the Mathematical Library of an UAV Autopilot with Frama-C. In:Proc. of the Int'l Conf. on Formal Methods for Industrial Critical Systems. 2021. 167-173.[doi:10.1007/978-3-030-85248-1_10]
    [16] Ma ZW, Chen G. Matrix formalization based on Coq record. Computer Science, 2019, 46(7):139-145(in Chinese with English abstract).[doi:10.11896/j.issn.1002-137X.2019.07.022]
    [17] Ma YY, Ma ZW, Chen G. Formalization of operations of block matrix based on Coq. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6):1882-1909(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6255.htm[doi:10.13328/j.cnki.jos. 006255]
    [18] Wang YF, Chen G. Formalization of Laplace transform in Coq. In:Proc. of the 2017 Int'l Conf. on Dependable Systems and Their Applications (DSA). 2017. 13-21.[doi:10.1109/DSA.2017.12]
    [19] Wang YF, Chen G. A formal proof of two properties of Laplace transform. In:Proc. of the 2018 IEEE Int'l Conf. of Safety Produce Informatization (IICSPI). Chongqing, 2018. 883-887.[doi:10.1109/IICSPI.2018.8690475]
    [20] Ma ZW, Chen G. Formal derivation and verification of coordinate transformations in theorem prover Coq. In:Proc. of the 2017 Int'l Conf. on Dependable Systems and Their Applications (DSA). 2017. 127-136.[doi:10.1109/DSA.2017.29]
    [21] Bertot Y, Casteran P. Interactive Theorem Proving and Program Development:Coq'Art:The Calculus of Inductive Constructions. Springer, 2004.
    [22] Coq Development Team. The Coq Reference Manual 8.13.2.
    [23] Pierce BC, et al. Software Foundations Volume 1. https://softwarefoundations.cis.upenn.edu/
    附中文参考文献:
    [2] 全权.多旋翼飞行器设计与控制.北京:电子工业出版社, 2018.
    [5] 徐敏.空气动力学基础.第2版,西安:西北工业大学出版社, 2015.
    [6] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报, 2019, 30(1):33-61. http://www.jos.org.cn/10000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [7] 陈钢,施智平.形式化工程数学.中国计算机学会通讯, 2017, 13(10).
    [8] 陈钢.形式化数学和证明工程.中国计算机学会通讯, 2016, 12(9).
    [16] 马振威,陈钢.基于Coq记录的矩阵形式化方法.计算机科学, 2019, 46(7):139-145.
    [17] 麻莹莹,马振威,陈钢.基于Coq的分块矩阵运算的形式化.软件学报, 2021, 32(6):1882-1909. http://www.jos.org.cn/1000-9825/6255.htm[doi:10.13328/j.cnki.jos.006255]
    引证文献
引用本文

石正璞,崔敏,谢果君,陈钢.多旋翼飞控推进子系统的Coq形式化验证.软件学报,2022,33(6):2150-2171

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-03
  • 最后修改日期:2022-02-25
  • 在线发布日期: 2022-06-09
  • 出版日期: 2022-06-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号