A Research On Modeling And Implementation Based On The End To End Flow Of AADL

In real-time systems,the correctness of system behavior depends not only on the correctness of computation results but also on the correctness of the time at which the results are produced.End-to-end latency is an important measure for system time constraints.End-to-end latency is influenced by various factors,such as oversampling,undersampling,resource contention,and task execution jitter.To mitigate these effects,the model-driven development approach can be adopted to ensure time constraints at critical stages such as requirement analysis,design verification,and code implementation,thereby reducing the cost of system development.Additionally,the LET task theory can be introduced within the system to finely ensure time constraints at the task level.AADL is a standard architecture description language commonly used in modeldriven development.It features a clear capability to describe real-time behaviors and provides a unified semantic representation for system development.However,the simulation verification method in AADL requires the simulation of specific execution paths to calculate end-to-end latency,which necessitates the completion of the code implementation phase.Therefore,the primary challenge of using AADL in system development is the lack of model verification algorithms suitable for the system design phase.This paper aims to form a real-time system development method for model-driven development at key stages focused on the end-to-end latency constraint of the AADL model for LET systems.This method takes the AADL end-to-end latency to ensure task chains’ real-time behavior and LET tasks to ensure individual task’s real-time behavior.The specific research results are as follows:1.A set of pattern-based transformation paradigms are provided to form a formal expression of natural language requirements and simplify TCTL verification syntax.Firstly,based on the AADL end-to-end latency constraint semantic definition,the requirement expression pattern is defined,which consists of three dimensions:"pattern scope-pattern category-real-time attribute," used for classifying natural language requirements.Then,this method formally implements the observer model based on the timed automata theory to simplify the check for state and clock by converting it into checking for error state reachability.This method provides an efficient and concise requirement analysis verification method in the requirement analysis stage.2.Design verification:AADL2TA model transformation method is proposed to verify end-to-end latency based on model checking algorithms.Firstly,an AADL metamodel for modeling LET systems is proposed based on the LET task theory,and a model transformation method for converting component-defined AADL to timed automata is proposed.Considering the composability of LET tasks,an abstract component relationship graph is obtained by extracting the organization structure of the AADL model,and an algorithm for combining independent TAs into a TA network is proposed.At the same time,based on the trajectory consistency theory,it is proved that the two models are functionally equivalent.This method solves the problem that the AADL simulation verification method cannot be applied in the design stage.3.System implementation:A code generation scheme for ensuring end-to-end latency based on the AADL design model in the real-time operating system FreeRTOS environment is proposed.Periodic and sporadic tasks are implemented by extending FreeRTOS’s task management services,and LET task’s data input,output,and calculation parts are defined.Meanwhile,task read and write primitives are defined based on the queue to support LET tasks in the system.Based on this,the executable system program is obtained by initializing tasks and starting the scheduler.Finally,this paper presents the experimental results of the unmanned autonomous flight system PapaBench in the three phases mentioned above,which validates the feasibility of the proposed method.Furthermore,by comparing the end-to-end latency verification results of AADL2TA with AADL simulation,it is shown that our method can provide accurate end-to-end latency property verification results during the design phase,thereby demonstrating the effectiveness of the proposed method.