In the development of safety critical systems such as large civil aircraft, the increase of system complexity has greatly reduced the efficiency and effectiveness of traditional safety assessment methods by the experience of designers, and brought problems such as iterative difficulty. A novel safety assessment method called Model-Based Safety Assessment (MBSA) can significantly reduce development analysis complexity and improve the efficiency of safety assessment work. On the other hand, MBSA related safety assessment work has also been added in ARP 4761A. Based on the above background, this paper explains the basic principle of formalized security model, the basic principle of safety evaluation, detailed analysis process and the method of safety requirements definition by using finite state machine and temporal logic. A civil aircraft was taken as an example,the SMV formal model was established and the formal safety requirements of aileron control function were defined. This paper presents a case of the safety verification, and proves the feasibility of formal method based safety assessment in the security work of civil aircraft system.