Design And Implementation Of AADL Model Schedulability Analysis Tool

As the field of application based on computer extends increasingly, the scale of developing computer software and the complexity of software increase, so it is the same with the time and cost of developing. Aiming at solving these problems, Object Management Group (OMG) proposes Model Driven Architecture (MDA). The core idea of MDA is to separate the model with the realization, so that the procedure of software developing can be simplified into building up business logical model then creating code on specific computing platform automatically by machine. Therefore, the modeling language in MDA is not only designing language but also programming language.The industry has put out a modeling language based on MDA method for developing embedded system software---Architecture Analysis and Design Language (AADL), against the similar problems from the software complexity. AADL is a modeling language which can be used to design and analyze the software and hardware architecture of performance-critical real-time systems. The developing platform and the model verification tool around AADL are becoming the developing hot point.The most important part in MDA is model, which needs other tools to test if the designing fits the original demand. This thesis is based on hybrid automaton with relative time constraints, designing a kind of verification tool to do a formal test on AADL model's schedulability.First of all, this thesis gives an introduction of research situation and existing tools for AADL model schedulability's verification and analysis of the defect of each tool, then a brief introduction of AADL concept and timed automaton theory. The practice using UPPAAL tool to verify AADL model schedulability shows that UPPAAL can not verify AADL model schedulability under the preempt dispatch strategy.Therefore,the thesis designed UCaS tools for AADL model schedulability verification based on hybrid automaton with relative time constraints theory. The UCaS design, related technology and key code are particularized with soft engineering method. A performance test for UCaS tool is also realized. Last, this paper summarized advantage and limitation of UCaS tools and give a outlook for AADL model verification tools further research and development.