Research on formal verification technique for aircraft safety-critical software

As an important part of airborne avionics system, aircraft safety critical software (ASCS) plays an essential role to the safety of the aircraft, and to ensure its quality and reliability is one of the key problems we are facing. Formal methods have become important means for modeling and verifying safety critical software. In this paper, formal method is introduced into the ASCS verification field and the real-time extended finite state machine model (RT-EFSM) is studied, which includes the detailed real-time extension schemes and its validation methods. The verification process of ASCS based on RTEFSM is also proposed. Furthermore, combined with the verification of an aircraft inertial/satellite navigation systems, a timed unique input/output sequence (t_UIO) is presented and the automatic generation algorithm of subtransfer sequences based on t_UIO is given. Finally, the test adequacy criteria are discussed and a time condition coverage criterion is proposed. The actual engineering project application shows that the method proposed in this paper is of great value for the ASCS, which can be generally and effectively used in engineering.