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 verifcafion an...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 verifcafion 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 arias 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.展开更多
Cyber-physical systems(CPSs)are becoming increasingly important in safety-critical systems.Particular risk analysis(PRA)is an essential step in the safety assessment process to guarantee the quality of a system in the...Cyber-physical systems(CPSs)are becoming increasingly important in safety-critical systems.Particular risk analysis(PRA)is an essential step in the safety assessment process to guarantee the quality of a system in the early phase of system development.Human factors like the physical environment are the most important part of particular risk assessment.Therefore,it is necessary to analyze the safety of the system considering human factor and physical factor.In this paper,we propose a new particular risk model(PRM)to improve the modeling ability of the Architecture Analysis and Design Language(AADL).An architecture-based PRA method is presented to support safety assessment for the AADL model of a cyber-physical system.To simulate the PRM with the proposed PRA method,model transformation from PRM to a deterministic and stochastic Petri net model is implemented.Finally,a case study on the power grid system of CPS is modeled and analyzed using the proposed method.展开更多
首先归纳了AADL(architecture analysis and design language)的发展历程及其主要建模元素.其次,从模型驱动设计与实现的角度综述了AADL在不同阶段的研究与应用,总结了研究热点,分析了现有研究的不足,并对AADL的建模与分析工具、应用实...首先归纳了AADL(architecture analysis and design language)的发展历程及其主要建模元素.其次,从模型驱动设计与实现的角度综述了AADL在不同阶段的研究与应用,总结了研究热点,分析了现有研究的不足,并对AADL的建模与分析工具、应用实践进行了概述.最后,探讨了AADL的发展与研究方向.展开更多
提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础...提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.展开更多
针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性...针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.展开更多
结构分析与设计语言(architecture analysis and design language,AADL)是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。针对系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显突出的问题,给出了一个基于AADL的软件...结构分析与设计语言(architecture analysis and design language,AADL)是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。针对系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显突出的问题,给出了一个基于AADL的软件系统可靠性建模与评估框架:首先建立AADL可靠性模型,然后将其转换为广义随机Petri网(generalized stochastic Petri net,GSPN)模型后再进行分析,最后根据分析结果判断是否需要进行模型改进。在研究已有的基本转换规则的基础上,重点讨论了系统中组件之间错误传播以及表示系统发生模式转换的Guard_Transition属性到GSPN的转换规则。以某飞行控制系统中数据发送和处理单元为实例,验证了所提转换规则和可靠性建模与评估框架的有效性。展开更多
为了支持新一代航电系统在体系结构设计阶段进行系统可靠性分析和评估,对复杂嵌入式系统利用体系结构分析与设计语言(architecture analysis and design language,AADL)进行系统的建模。提出了一种基于AADL系统体系结构模型的可靠性建...为了支持新一代航电系统在体系结构设计阶段进行系统可靠性分析和评估,对复杂嵌入式系统利用体系结构分析与设计语言(architecture analysis and design language,AADL)进行系统的建模。提出了一种基于AADL系统体系结构模型的可靠性建模方法,设计出一套转换规则,对AADL体系结构模型的软硬件构件进行模型转换,实现从AADL系统体系结构可靠性模型到系统体系结构广义随机Petri网(system architecture general stochastic Petri net,SAGSPN)的转换,并基于加权的SAGSPN可靠性计算模型对系统进行可靠性评估。最后通过对某飞控系统进行可靠性评估,验证了方法的有效性,证明该方法对航电系统的体系结构设计提供了支持。展开更多
基金National Natural Science Foundations of China (No. 61073013,No. 90818024)Aviation Science Foundation of China(No.2010ZAO4001)
文摘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 verifcafion 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 arias 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.
基金the State Power Grid Company Science and Technical Plan Project,China(No.5100-201940008A-0-0-00)。
文摘Cyber-physical systems(CPSs)are becoming increasingly important in safety-critical systems.Particular risk analysis(PRA)is an essential step in the safety assessment process to guarantee the quality of a system in the early phase of system development.Human factors like the physical environment are the most important part of particular risk assessment.Therefore,it is necessary to analyze the safety of the system considering human factor and physical factor.In this paper,we propose a new particular risk model(PRM)to improve the modeling ability of the Architecture Analysis and Design Language(AADL).An architecture-based PRA method is presented to support safety assessment for the AADL model of a cyber-physical system.To simulate the PRM with the proposed PRA method,model transformation from PRM to a deterministic and stochastic Petri net model is implemented.Finally,a case study on the power grid system of CPS is modeled and analyzed using the proposed method.
文摘首先归纳了AADL(architecture analysis and design language)的发展历程及其主要建模元素.其次,从模型驱动设计与实现的角度综述了AADL在不同阶段的研究与应用,总结了研究热点,分析了现有研究的不足,并对AADL的建模与分析工具、应用实践进行了概述.最后,探讨了AADL的发展与研究方向.
文摘提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.
文摘针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.
文摘结构分析与设计语言(architecture analysis and design language,AADL)是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。针对系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显突出的问题,给出了一个基于AADL的软件系统可靠性建模与评估框架:首先建立AADL可靠性模型,然后将其转换为广义随机Petri网(generalized stochastic Petri net,GSPN)模型后再进行分析,最后根据分析结果判断是否需要进行模型改进。在研究已有的基本转换规则的基础上,重点讨论了系统中组件之间错误传播以及表示系统发生模式转换的Guard_Transition属性到GSPN的转换规则。以某飞行控制系统中数据发送和处理单元为实例,验证了所提转换规则和可靠性建模与评估框架的有效性。
文摘为了支持新一代航电系统在体系结构设计阶段进行系统可靠性分析和评估,对复杂嵌入式系统利用体系结构分析与设计语言(architecture analysis and design language,AADL)进行系统的建模。提出了一种基于AADL系统体系结构模型的可靠性建模方法,设计出一套转换规则,对AADL体系结构模型的软硬件构件进行模型转换,实现从AADL系统体系结构可靠性模型到系统体系结构广义随机Petri网(system architecture general stochastic Petri net,SAGSPN)的转换,并基于加权的SAGSPN可靠性计算模型对系统进行可靠性评估。最后通过对某飞控系统进行可靠性评估,验证了方法的有效性,证明该方法对航电系统的体系结构设计提供了支持。