This is an on-going project

• created at: July 13, 2022*

• What is VFCS?
  • Verified Flight Control System (VFCS) is an academic project for study the FCS software by theorem prover Coq.
  • We adopt the idea of construct-correct to analysis, modeling and design the FCS.
  • Coq proof assistant is a higher-order logic theorem prover based on Calculus of Inductive Constructions.
  • We mainly study the Multicopter at the first stage.
• Why start the project ?
  • FCS is a safety critical software system, and it's reliability is hard to promise by traditional Disign-Build-Test aproch.
  • The FCS is a comprehensive engineering system, and many special knowledge, experience data and mathematical theory need to be formal described , organized and verified. Meanwhile, these knowledge and theory are existed in many similiar system.
  • So, it is a fundamental research topic with huge potential benefits
• Who are we?
  • We are a team focused on the study of formal engineering mathematics, located in Nanjing University of Aeronautics and Astronautics in China.
  • Authors list Zhengpu Shi ([email protected])

• Dependent projects:
  • CoqExt: Extension of Coq Standard Libray. [Homepage]
  • CoqMatrix: Formal matrix theory with multiple implementations in Coq.
• Related projects:

Note: most of them are Chinese version.

• Text books
  • 自动控制原理，清华大学出版社，卢京潮
  • 复变函数与积分变换，华中科技大学，李红
  • Control Systems Engineering, by Norman S. Nise
  • 控制工程基础，高教出版社，王积伟、吴振顺
• Resources from Internet
  • Bilibili 自动控制原理
  • Bilibili 复变函数与积分变换