A Method For Extension And Verification Of AADL Behavior Annex In The Context Of Hierarchical Behavior Modeling

AADL is a modeling language to describe embedded real-time systems and is widely used to model safety-critical systems.AADL presents the system models hierarchically through components such as systems,processes,and threads,etc.The Behavioral Annex is a supplement of AADL in terms of functional behavior,and it enables modeling of component and component interaction behavior in a state-machine based annex sublanguage.At present,there is no mechanism to represent hierarchical automata for the behavior annex.However,this is a very important feature because the industrial complex systems are always described with composite states.Although we can model the system with AADL's own hierarchical description capabilities,it will result in a large-scale of threads.In the development process,designers often need to manually flatten the functional requirements described hierarchically and then model them with AADL behavior annex.This process is complicated and error-prone.The flattened state machine causes the loss of structural information and does not intuitively represent the level of inclusion of functional behavior modules.Aiming at this problem,this paper proposes a component functional behavior modeling and verification method based on AADL behavior annex,including two parts: hierarchical behavior annex modeling method and hierarchical behavior annex formal verification method.In order to meet the actual industrial modeling needs,this paper proposes a hierarchical extension of the AADL behavior annex--HBA firstly,gives the formal syntax of the HBA,and then defines the operational semantics of the HBA.The meta-model of HBA is proposed and its text and graphical editor is implemented in the OSATE environment.In order to verify the model,this paper proposes a formal verification method for hierarchical behavior annex.Firstly,the hierarchical behavior model is transformed into multiple associated flat automata through the hierarchical behavior annex flattening method,and then the hierarchical behavior model is converted into the Time Automaton Network through the hierarchical behavior annex to the time automaton conversion method,finally verifying the model by manually extracting the property related to the tested model.Finally,the effectiveness of the proposed method is verified by giving a spacecraft guidance navigation and control system case.Firstly,it is tested whether the proposed modeling method is suitable for modeling actual industrial cases by describing the modeling process in detail and refining the original requirements gradually.Then,it is tested whether the HBA formal verification method proposed in this paper can detect the inconsistency between the model and the property by pre-burying the error in the original requirements.