A Compositional Verification Method For AADL Models Of Safety-critical Software

With safety-critical software the growing size and complexity,ensure that the software design and functional correctness becomes more difficult.Model-driven development methods have become the main means for the design and development of safety-critical software,and AADL(Architecture Analysis and Design Language)as an architecture and analysis language standard for complex embedded systems,is widely used in the modeling of software and hardware architectures,runtime environments,functional and non-functional attributes of safety-critical software.AADL can naturally hierarchical decomposition the hierarchy of complex safety-critical software,and can manage the complexity of the system abstractly through a hierarchical method.In industrial applications,how to complete the complex and hierarchical AADL model verification is an urgent problem to be solved,and the traditional AADL model verification method is often to convert the flat entire model and then directly verify it.The state space unfolding has the problem of state space explosion when verifying the AADL model of complex systems.This paper proposes a compositional verification method for AADL models for safety-critical software.It focuses on the key issues of combination verification of AADL architecture models and functional behavior verification of AADL components,and designs and develops prototype tools for AADL model verification.The main research results are as follows:Firstly,a combination verification method of the AADL architecture model is proposed,and the system AADL architecture model is constructed based on the system level decomposition,and then the component requirements of each level of the system are formalized into component contracts,that is,abstract externally visible behaviors.The system architecture model is verified to verify the correctness of the system architecture.Secondly,the AADL2 UPPAAL model conversion method is proposed to convert the AADL model to the UPPAAL model to verify and analyze the functional behavior of the leaf components of the architecture model.UPPAAL uses time automatically as the theoretical basis,and uses time calculation tree logic to support functional correctness,reachability,safety and other properties.Finally,based on the open source modeling environment OSATE,the AADL model verification prototype tool was designed and implemented,supporting the combined verification of the architecture model based on AGREE and the functional behavior verification of components based on UPPAAL.Then a combination of AGREE and UPPAAL was used to verify the actual cases in the industry.The effectiveness and limitations of the AADL combination verification tool are analyzed by analyzing actual cases in the industry.Through the above verification method,not only the functional correctness of the single component is guaranteed,but also the correctness of the architecture of the entire system.