Automatic flight control system （AFCS） is one of the most important safety-critical systems in modern aircraft， and flight guidance control system （FGCS） is an important part of it. There are dozens of flight modes in FGCS， and its mode conversion logic is very complex， which is prone to pattern confusion and other problems in the conversion of various modes， making it difficult to verify their safety and correctness. However， formal modeling and verification of safety-critical systems can improve the correctness and safety of the system by using formal methods in computer science. This paper takes the automatic flight mode conversion logic of typical FGCS as the research object， uses the software tool ART （Avionics requirement tool） independently developed by the author team to carry out formal modeling and verification， and compares the verification ability and efficiency with the Design Verifier tool in Matlab/Simulink. The case study results show that it is feasible to model and verify the automatic flight mode conversion logic of FGCS using formal methods. Meanwhile， our software platform has more complete verification capability and better verification efficiency.