Abstract: DO-333 is the formal supplement to the aircraft software’s safety standard DO-178C,which provides gui-dance for the use of formal methods in the development process of aircraft software.Model checking,as a kind of formal methods,can be applied for the strict verification of the software artifacts in the requirement and design phase.Based on DO-333,this paper used model checking to formally verify the software artifacts of different development phases for a slats and flaps control unit,one component of the flight control system,aiming to justify whether the software artifact satisfies the related objectives or not in DO-178C and provide the evidence support.Firstly,model checking is applied to the specification and verification of the high_level requirements for the mutual updating operation between flap and slat.Then,it is applied to the low_level requirements for the control logic in a single wing.Based on the verification and analy-sis above,evidence is provided for the verification objectives about high_level and low_level requirements in DO-178C.This paper illustrated an application example of model checking in an aircraft software’s certification and could provide technical support for the safety assurance and airworthiness certification of aircraft software.

Key words: Airworthiness certification,Formal methods,Model checking,Aircraft software,SPIN