¹ Department of System Engineering of Engineering Technology, Beihang University, Beijing, China
² Center of Aviation Safety Technology, Civil Aviation Administration of China, Beijing, China

---

Abstract—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.

Index Terms—real-time embedded software; aircraft; safety critical software; RT-EFSM; formal methods; verification; test sequence

[PDF]

Cite: Yongfeng Yin, Bin Liu, and Duo Su, " Research on Formal Verification Technique for Aircraft Safety-Critical Software," Journal of Computers vol. 5, no. 8, pp. 1152-1159, 2010.