AADL Model Transformation And Validation Studies

Along with the computer application domain unceasing expansion, the computer software development scale has gradually broadened, and the complexity of software is increasing. It leads to the development cycle and development cost increase. In order to solve these problems, the Object Management Group (OMG) put forward a new method-Model Driven Structure (MDA) method. The core idea of MDA is using the system model as center; the system model is separated from the system implementation. By this way the software development process is simplified for establishing the business logic model and it can automatically generate code on the specific computing platform. In MDA, modeling language is not only a design language; but also a programming language.In the real system modeling field, the industry proposed an Architecture Analysis and Design Language AADL, which is based on the MDA idea. The AADL is a modeling language which is mainly used to design the software and hardware architecture of crucial real-time system. As the AADL can describe system precisely, it has gradually become the standard in real-time software development. This paper mainly studied the AADL model transformation and model verification. This article was divided into three parts focus on illustration.First, this paper studies the AADL standard semantics, because the AADL formal semantic is described inadequately, then it discusses formal verification methods on AADL model. Through researching on the AADL model schedulability and reliability verification theory, it summed up the general verification method of AADL model. The method is translating AADL model into a formal model, and use the existing formal verification tools to validate. As well it introduces a formal modeling language BIP, which is a component-based real-time system modeling framework.Second, according to the MDE perspective, two heterogeneous model transformations conform to the general idea, semantic layer mapping and syntax form conversion. Therefore it proposes the use of the ATL meta-model transformation language and EMF frameworks, translate AADL application model into BIP model. It formulates the relevant mapping rules and gives some examples. Third, for the AADL execution semantics, it introduces the details of using the BIP modeling AADL thread, after it explores the theory of BIP model validation and verification tools. These can validate the BIP model reliability and safety.By do that, it can indirectly ensure AADL model security.AADL model transformation and verification can help designer find out the system defect in early development. It can greatly improve the efficiency of system development, at the end of the paper it concludes that large-scale application of this method still have some problems need to be resolved, and it points out the research directions in the future.