多旋翼飞控推进子系统的Coq形式化验证

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

Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter

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 paper 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 and 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; generated a functional software library 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.