End-to-end Flow Modeling And Verification For Avionics Systems

Avionics systems are a class of safety-critical systems with complex system architectures that place high demands on system quality and play a dominant role in allocating processor resources,scheduling real-time tasks and sharing storage resources.The architecture of such systems typically consists of multiple interrelated tasks that process data from sensors to actuators.From the design phase of an avionics system,it is important to assess whether the information meets its timing requirements.One important design parameter is the end-to-end delay of the information,which needs to be within specified limits to ensure the correct operation of the avionics system.In this paper,in order to satisfy the end-to-end delay constraints of avionics systems and to support the formal modelling and verification of end-to-end flows in avionics systems,a data flow modelling method for safety-critical systems,the Sys ML flow model,is proposed on the basis of Sys ML,and a transformation method is investigated to convert the Sys ML flow model into a time automaton for analysis and verification.The main contributions of this paper include.· A Sys ML flow model for end-to-end flows of avionics systems is proposed.The formal syntax and semantics of the Sys ML flow model are defined to support the analysis and verification of delay type requirements in avionics systems.· proposes a method for converting the Sys ML flow model into a temporal automaton for schedulability and end-to-end delay verification.Time-computing tree logic statements are designed for verifying the schedulability and end-to-end stream delay properties of the system.· Designed and implemented a modelling tool based on the Sys ML flow model to support the modelling and verification of the Sys ML flow model.The Sys ML flow modelling technique was applied to a longitudinal flight control system for verification and analysis,illustrating the specific application of Sys ML flow modelling to avionics systems.The approach provided by this research provides delay analysis from a high level specification without the need to implement the system,saving potential redesign efforts.It also allows Sys ML flow models to be deployed in avionics systems in different ways to ensure that the end-to-end delay requirements of avionics systems can be met.Sys ML flow models and Sys ML flow model modelling tools have an important role to play in extending the use of model-driven architectures and their application in safety-critical avionics systems.