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 (zhengpushi@nuaa.edu.cn)
- Dependent projects:
- Related projects:
Note: most of them are Chinese version.
- Text books
- 自动控制原理，清华大学出版社，卢京潮
- 复变函数与积分变换，华中科技大学，李红
- Control Systems Engineering, by Norman S. Nise
- 控制工程基础，高教出版社，王积伟、吴振顺
- Resources from Internet
- Bilibili 自动控制原理
- Bilibili 复变函数与积分变换