In the field of safety-critical systems, explicit requirements for the system are essential. We use model-based system engineering idea to model and verify the automatic flight control system (AFCS) based on system requirements. We employ the RSML-e language to model the requirements of the AFCS , propose a method to transform the RSML-e model to NuSMV 2 model, and use the NuSMV 2 to verify the properties of the requirement model. Taking a digital AFCS-GFC700 as an example, we analyze and verify the model. Experimental results show that the method is feasible for the safety analysis of actual systems.

 

 

MBSE, automaticflight control system (AFCS), formal verification, RSML-e, NuSMV, model transformation