采用AADL的软件系统可靠性建模与评估方法

结构分析与设计语言(architecture analysis and design language,AADL)是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。针对系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显突出的问题,给出了一个基于AADL的软件系统可靠性建模与评估框架:首先建立AADL可靠性模型,然后将其转换为广义随机Petri网(generalized stochastic Petri net,GSPN)模型后再进行分析,最后根据分析结果判断是否需要进行模型改进。在研究已有的基本转换规则的基础上,重点讨论了系统中组件之间错误传播以及表示系统发生模式转换的Guard_Transition属性到GSPN的转换规则。以某飞行控制系统中数据发送和处理单元为实例,验证了所提转换规则和可靠性建模与评估框架的有效性。     

系统架构描述语言AADL的功能行为建模扩展

架构分析与设计语言(AADL)是一种用于描述复杂嵌入式系统体系架构的建模语言,被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为,而行为附件中没有表达层次自动机的机制。针对这一问题,提出了AADL行为附件的层次化扩展——HBA。首先给出了HBA的形式语法,然后定义了HBA的操作语义。提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了便于形式化验证,给出了HBA到时间自动机(TA)的转换规则,并基于模型检测工具UPPAAL进行形式化验证。最后,给出一个案例研究来验证所提方法的有效性。     

AADL建模工具的设计

设计一种架构分析与设计语言(AADL)建模工具,便于用户建立AADL模型.基于模型驱动体系结构思想,在Eclipse插件开发平台上开发可扩展的插件集合AADL模型设计工具.用户根据该工具建立的嵌入式系统AADL架构模型,通过XML文档保存,分析与验证工具以第三方插件的形式集成到该工具中,提取系统的AADL架构模型.通过应用实例验证了该工具的有效性.     

复杂嵌入式实时系统体系结构设计与分析语言:AADL

首先归纳了AADL(architecture analysis and design language)的发展历程及其主要建模元素.其次,从模型 驱动设计与实现的角度综述了AADL 在不同阶段的研究与应用,总结了研究热点,分析了现有研究的不足,并对 AADL 的建模与分析工具、应用实践进行了概述.最后,探讨了AADL 的发展与研究方向.     

AADL分级调度模型的分析与验证

针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.     

安全关键软件的AADL模型自动逆向构造方法

近年来,采用模型驱动(Model-Driven)尤其是形式化模型驱动的安全关键软件设计与开发方法逐渐受到重视,并被工业界认为是切实可行的重要手段.AADL(Architecture Analysis and Design Language)是一种广泛应用于安全关键领域的形式化建模语言标准.在安全关键软件系统开发与维护过程中,部分需求与设计信息往往遗留在源代码中,在对已有软件系统架构进行复用或重构的过程中,如何将这部分需求与设计信息从代码中构造到设计模型是一个重要问题.本文基于模型驱动逆向工程,提出一种从C代码到AADL模型的自动构造方法C2AADL.首先分析了源语言结构、行为和运行时性质,并根据分析结果提出了源代码结构、行为和运行时性质到AADL模型的转换规则,然后根据转换规则设计并实现了原型工具,最后基于雷达信息处理子系统案例验证本文所提方法的有效性.     

基于AADL的CPS系统分析与设计

信息物理融合系统CPS(Cyber Physical System)的建模需要融合离散计算实体与连续物理实体,而传统的建模方法却是分别对两者进行建模,缺乏对两者相互融合的抽象。针对这种情况,利用结构分析与设计语言AADL(Architectural Analysis and Design Language)在基于模型开发上的优势,对AADL所不能支持的时空、行为、动态连续等方面进行扩展,通过比较现有元胞自动机、Modelica与AADL的区别与关联后,提出相应的变换公式将两者用AADL的形式表达。以车联网CPS系统为案例,详细描述系统的组成与建模过程,并对该模型在系统体系结构、端到端的流延迟等方面进行分析验证,证实该方案的可行性与正确性。     

Research on Verification Method of AADL Behavior Model Based on UPPAAL

为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则.在转换规则的基础上,设计和实现了自动转换的原型工具.最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例,经自动转换得到时间自动机模型,并在UPPAAL下仿真、验证其行为正确性,同时证明了模型转换的有效性.     

基于AADL的中断控制设计方法

介绍了结构分析与设计语言(AADL)的应用研究和优点,以某航天器控制分系统部分中断类型为例,针对AADL语言自身直接对中断问题描述能力上的不足,提出了两种基于AADL的中断控制设计方法,并进行了详细阐述和比较,为系统设计阶段对中断控制的抽象描述提供了一种思路和方法,从而有利于实现早期阶段对模型可调度性等方面验证的途径.     

基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具，可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而，AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果，尤其是对于资源动态分配的实时系统。为解决结果不精确的问题，可结合基于系统有穷状态空间遍历的模型检验方法。首先，将实时系统AADL模型转换为时间自动机(TA)模型，以TA为理论体系进行模型检验。其次，基于反应链的需求分类定义端到端延迟需求表达模式。最后，给出对应需求模式的观察者模型，与系统模型并行组合，优化模型验证的时空资源消耗。     

AADL模型的代码自动生成及集成技术

体系结构分析设计语言（AADL）是一种基于模型驱动体系结构的建模语言,针对如何将AADL模型自动生成框架代码的问题,提出AADL模型元素同C语言元素间的转换规则,设计AADL模型转换为C语言框架代码的自动代码生成器Generator。实例证明了AADL模型自动转换为可执行C代码的有效性。     

AADL+: a simulation-based methodology for cyber-physical systems

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system architectures. It is quite popular for its simple syntax, powerful functionality and extensibility and has been widely applied in embedded systems for its advantage. However, it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic behaviors. This paper proposes an approach to construct a new sublanguage of AADL called AADL+, to facilitate the modeling of not only the discrete and continuous behavior of CPS, but also interaction between cyber components and physical components. The syntax and semantics of the sublanguage are provided to describe the behaviors of the systems. What’s more, we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of CPS. And the plug-in supports syntax checking and simulation of the system model through linking with modelica. Finally, the AADL+ annex is successfully applied to model a lunar rover control system.     

基于UPPAAL的AADL模型可调度性验证

针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言,基于形式化理论的本方法的验证结果更加精确。     

基于AADL的IoP系统可靠性评估方法

人联网（IoP）系统的架构复杂且存在海量、实时变化的数据,使得基于IoP系统的可靠性分析变得十分困难,目前仍缺乏一种健全的基于IoP系统的可靠性建模及评估方法。提出一种新型的IoP系统可靠性评估方法,利用AADL及其附件语言对IoP系统进行可靠性建模,并基于该模型从定性角度评估系统故障的根本原因和风险。此外,结合Ocarina模型转换技术提出一种基于连续时间马尔科夫链（CTMC）的定量评估算法,将AADL可靠性模型转换为CTMC模型,实现对系统动态、实时等特性的评估。在此基础上,设计一个IoP系统通用模型,并以此为案例验证所提方法的可行性。实验结果表明,该方法不仅能对IoP系统建模,而且能自动、准确地对其进行可靠性分析,具有良好的应用价值。     

基于Uppaal的实时系统AADL数据流模型的转换与验证

体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。     

AADL模式转换设计方法研究

为实现AADL(体系结构分析与设计语言)对航天器控制系统等运行模式相对复杂的嵌入式系统的详细描述,针对AADL核心标准及其行为附件在描述能力上的不足,在行为附件原有文法定义的基础上进行改进,使之能够对多条件合集下的模式转换以及模式转换的优先级进行描述。提出了抽象状态的概念以简化原行为附件文法在描述组合式状态转换关系方面的繁杂程度,提高设计模型的可读性。通过对实际控制系统运行模式进行设计,结果表明了改进后的行为附件文法很好地满足了设计描述上的需求。     

AADL进程子集行为语义研究

AADL是一种基于组件的半形式化建模语言,采用结构化方法对大型复杂软件系统的软硬件进行统一建模,有效描述系统的功能行为、非功能属性以及运行时的体系结构动态演化,但其许多问题需要进一步研究与完善。本文首先分析了AADL形式语义研究现状,然后定义了AADL进程子集的形式语言,建立了AADL进程子集通信模型,通过对事件的形式化定义和分析体现了事件在系统状态转变过程中的重要作用,对AADL进程子集行为语义进行了研究。与相关研究成果的对比说明了本文的优势。本文为AADL语言及其形式语义的发展提供了一种有益的参考,进一步完善大型复杂软件系统体系结构建模与分析技术。