关键词: 形式化验证, RSML-e, Lustre, 模型转换, 安全性, 自动飞行系统

Abstract: The automatic flight system is the core system of flight control for modern large aircraft.The flight guidance system,as the core subsystem of the automatic flight system,manages and controls the mode transition of the automatic flight system.The different flight stages of an automatic flight system are essentially flight mode transition,which determine the flight safety of the aircraft.However,flight mode transition has the essential characteristics of a multi-dimensional complex static structure that is coupled and compatible,as well as a multi-level dynamic combination of interactive cooperation and transitional switching.Therefore,ensuring the correctness of flight mode transition is of crucial importance.The model-driven software modeling method models the flight mode transition requirements as semi-formal or formal models,thereby analyzing and verifying the properties satisfied by the model.The existing methods face two challenges:1)The modeling from natural language requirements to semi-formal requirement models is mostly done manually,and there are differences among the requirement models established by different modeling languages;2)The semi-formal requirements model cannot be directly used for model checking.It needs to be transitioned into the input model of the model checking tool,and the verification efficiency of different verification tools also varies.Based on the RSML^-e requirement model of automatic flight mode transition,this paper proposes a systematic method for transitioning the RSML^-e model into the Lustre synchronous data flow language.Firstly,mapping rules are constructed from multiple dimensions such as data types,variables,logical phrases,AND-OR tables,and macros.It transitions the elements in the RSML^-e model one by one into the forms supported by the Lustre synchronous data stream language,and reduces the number of variables when describing the safety properties.Secondly,after the model transition,the Lustre model and safety properties obtained from the transition are input into the Jkind model checking tool for verification.Based on the various optimization techniques built into the Jkind model checking tool,the problem of state space explosion during the model verification process is better alleviated,and efficient verification of large-scale models is achieved.Ultimately,the safety properties related to the mode transition requirements of the automatic flight system are successfully verified through this process,ensuring the operational reliability of the system under various working conditions.

Key words: Formal verification, RSML^-e, Lustre, Model transition, Safety, Automatic flight system