AADL2TASM: a Verification and Analysis Tool for AADL Models

摘要

Architecture analysis and design language (AADL) is an architecture description language standard for embedded real-time systems and it is widely used in safety-critical applications. For facilitating verification and analysis, model transformation is one of the methods. A synchronous subset of AADL and a general methodology for translating the AADL subset into timed abstract state machine (TASM) were studied . Based on the atlas transformation language (ATL) framework, the associated translating tool AADL2TASM was implemented by defining the meta-model of both AADL and TASM, and the ATL transformation rules. A case study with property verification of the AADL model was also presented for validating the tool.