Design And Quantitative Analysis For Hybrid AADL Under Uncertain Environment

Due to the notable advantages like simple syntax,powerful function and good scal-ability,Hybrid Architecture Analysis and Design Language(AADL)has been proposed and used as the architecture model of Cyber-Physical Systems(CPS).The architecture model not only describes the hybrid behavior of the CPS,but also as a "golden reference model" to support the generation of the underlying implementation,so its correctness and reliability is the key to CPS construction.However,the worst-case performance analysis of Hybrid AADL designs often leads to overly pessimistic estimations,and is not suitable for accurate reasoning about overall system performance,in particular when the system closely interacts with an uncertain external environment.To address this challenge of modeling and analyzing the hybrid AADL under un-certain environment,this paper proposes a statistical model checking based framework that can perform quantitative evaluation of uncertainty-aware Hybrid AADL designs against various performance queries.It can effectively support the modeling of hybrid AADL,and enables quantitative analysis of hybrid AADL model.This thesis make three major contributions as follows:1.We extend the syntax and semantics of Hybrid AADL specifications using our proposed Uncertainty annex,which enables the accurate modeling of both per-formance variations caused by uncertain environments and performance require-ments specified by designers.2.To automate the quantitative analysis of uncertainty-aware Hybrid AADL designs,we rely on Network of Priced Timed Automata(NPTA)as the model of computa-tion in our approach.We propose a set of mapping rules that can automatically transform uncertain-aware Hybrid AADL designs into NPTA models and convert the performance requirements into various kinds of queries in the form of cost-constrained temporal logic.3.We designed and implemented the automated model transform tool AADL2UPPAAL.And based on our proposed SMC-based evaluation framework,we implement a tool chain that integrates both UPPAAL-SMC and the open-source AADL tool en-vironment OSATE to enable the automated performance evaluation and compar-ison of uncertainty-aware Hybrid AADL designs.Comprehensive experimental results on the Movement Authority(MA)scenario of Chinese Train Control System Level 3(CTCS-3)demonstrate that our proposed Uncer-tainty Annex can effectively model the uncertain environment,the quantitative analysis method can help AADL designers to analyze and select models from analysis result,the automatic model transform tool AADL2UPPAAL can accurate and fast support for quan-titative analysis.