Formal Modeling And Verification Of AADL Thread Component Using Real-Time Maude

With the development of the society and computer systems, computer systems have been widely used. Particularly in some domains such as aerospace, industrial control and automotive electronics, there are hard requirements on systems’ real-time performance and security. MDA(Model-driven Architecture) is a model-based system developmen-t method. MDA separates system design and implementation and is currently a major method in the development of complex computer system. AADL(Architecture Analysis & Design Language) is a modeling and analysis language for system architecture. AADL supports the specification and verification of system’s real-time performance and reliabili-ty. AADL is an instance of MDA method. It is a trend for design and analysis for complex compter system’archtecuture with AADL.Component is the modeling unit in AADL. AADL Thread component has runtime s-tates among AADL’s components. Thread is the scheduling unit and also the task’s carrier. The execution of threads can lead to changes in system states. Analysis and verification for AADL Thread’s behaviours on real-time performance and schedulability can contribute to the correctness of thread’s execution. Analysis and verification for the real-time perfor-mance and schedulability of complex computer system can contribute to finding errors of the model in the early stage of the development life cycle. This is very important for raising the development efficiency.Formal methods are mathematically based techniques for the specification, devel-opment and verification of software and hardware systems. Analysis and verifiaction for AADL Thread’s time-related properties is a major method for researches on AADL. This paper uses Real-Time Maude to formally model, verify and analyse AADL Thread. Real-Time Maude is an extension for formal language Maude and supports modeling and verification for real-time systems. Maude is based on rewrite logic and mainly used for modeling, model checking and logic deduction.In this dissertation, a modeling AADL Thread’s method is proposed. AADL Thread’s structure is modelled by the object-oriented modeling method in Real-Time Maude. And the transitions of runtime states in AADL Thread are modelled by rewrite rules in Real-Time Maude. The time-related properties of AADL Thread are verified with model check-ing tool in Real-Time Maude. This dissertation specified the EDF and RMS scheduling algorithms for AADL Thread’s real-time scheduling. With the formally specified EDF and RMS algorithms in Real-Time Maude, a method for verifying real-time schedulability of AADL Thread is proposed.The main contributions of the dissertation are applying Real-Time Maude to mod-el AADL Thread’s structure and time-related properties, modeling and verifying AADL Thread’s runtime states with Real-Time Maude’s rewrite rules and modeling EDF and RM-S algorithms for AADL Thread’s real-time schedulability with Real-Time Maude.