Research On Transition Rules Of AADL Subsets To TASM

With modernization, computer software has been widely used in aerospace, weapons, transportation and other safety-critical systems. a small logic error in the safety-critical real-time systems may lead to unforeseen catastrophic consequences, so ensuring the quality of the software system has become the urgent needs and challenges. Now, for safety-critical systems modeling, analysis and verification has become a hotspot of model validation direction.Architecture Analysis and Design Language(AADL) is a semi-formal modeling language, that is supported model engineering. AADL is a Language that can represent functional and non-functional requirements of safety-critical real-time systems, and has released a standard language library. However, due to the complexity of the AADL language and the semi-formal nature, selecting a subset of AADL and transiting the subset of AADL to a formal language,these are all we need to solve. TASM is a formal language that best describes the functional and nonfunctional behavior(such as execution time and resource consumption) of AADL models; and through a simple conversion operation, TASM can run on the verification and simulation tools (for example UPPAAL, TASM ToolSet and so on),confirm the system’s accuracy, consistency, scheduling and other non-functional performance verification.In order to achieve AADL model verification and analysis of the software components of safety-critical real-time system, this article selects a subset of the AADL and realizes AADL subsets’s formal conversion. The main work is as follows:Firstly, based on the AADL standard library, we choice a relatively complete subset of AADL based on the minimization principle, the realizability and the completeness principle, and describe elements of the subset of AADL.Secondly, AADL subsets formal conversion. this paper selected TASM as the formal language after transition. We implement formal conversion from AADL subsets to TASM, and complete subset to TASM conversion rules. we describe the rules using the form of pseudo-code. In the rules, we design conversion rules that is the thread withmulti-level scheduling protocol, complete building multi-level scheduling model.Finally, the flight control system on ARINC653 standard we use part of the system model as an example, using open source tool OSATE to achieve AADL to TASM conversion. we can validate the schedulability of multi-level scheduling system using UPPAAL, and verify the correctness of TASM transformation rules.