一种面向AADL架构的模型测试方法

鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构验证方法;该方法应用马尔可夫链描述AADL架构的行为,然后根据得到的马尔可夫链模型以及系统设计要求标准生成相应的测试用例和测试预言,并通过测试用例执行输出和期望值的比较判断AADL模型的正确性,实现对系统AADL模型的测试;最后通过案例分析证明了该方法的有效性。     

基于AADL的建模和验证技术应用研究

随着嵌入式系统规模、复杂度和性能需求的提升,嵌入式系统开发的重点从代码级提前到模型级;体系结构分析和设计语言AADL能够在模型级对系统进行建模,并通过一系列验证尽早发现系统设计中的问题,在航空航天等嵌入式系统中具有广阔的应用前景;全面系统地介绍了基于AADL的建模、验证的具体方法步骤、实现手段和工具,并以简化的飞行控制系统为例具体讲述了AADL的建模和验证技术的实际应用,从而为AADL技术在我国嵌入式软件中的应用奠定了基础。     

嵌入式软件系统体系结构可靠性分析方法

AADL是嵌入式领域对SA进行建模、评估的常用方法,但其属于一种半形式化开发语言,无法直接对SA的可靠性进行验证。为此,提出一种基于AADL的可靠性分析框架,对SA的可靠性进行形式化验证。首先通过分析系统体系结构的元素关系,建立AADL可靠性模型;然后设计转换模型及其规则,将AADL模型转换为连续时间马尔科夫链模型;最后采用概率模型检验工具对连续时间马尔科夫链模型进行可靠性定量分析。仿真结果表明,与现有可靠性分析方法相比,该方法在计算效率和转换效率上都有明显的提高。基于AADL的可靠性分析框架实现在软件系统开发早期对SA进行可靠性定量计算,为AADL在嵌入式软件系统可靠性定量分析方面提供了一种新的验证思路。     

基于STP方法的SCADE模型形式化验证框架

高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中。分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性。     

一种结合AADL和IMC的系统可靠性建模方法

随着嵌入式软件在安全关键领域广泛应用,系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显重要。结构分析设计语言AADL是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。由于AADL是一种半形式化模型,需要精确描述其语义才能进行定量分析。提出一种基于AADL的系统可靠性建模方法。首先,结合AADL模型和AADL错误模型附件,得到AADL可靠性模型;然后,提出一种模型转换方法,将AADL可靠性模型的基本元素和错误传播等特殊元素转换到交互式马尔科夫链模型IMC,进行可靠性定量分析;最后,结合法国空中交通控制系统的实例,证明该方法的可行性和有效性。     

AADL模型的形式化研究

在嵌入式系统建模领域,AADL以其软硬件协同建模的特点已经逐渐成为业界的标准。围绕AADL的形式化特点,国内外众多学者展开了热烈的讨论。为了帮助系统开发人员深入了解AADL,指导软件开发进程,提高基于AADL模型的软件开发效率,分别从AADL模型可靠性分析、可调度性分析以及AADL模型测试这三个不同角度综述了已经出现的各种AADL形式化验证理论,对比分析了它们的优点和不足。简要介绍有关AADL验证工具,研究基于AADL模型的嵌入式开发平台的构建。     

基于AADL的航天嵌入式软件Ada代码自动生成方法

模型驱动开发方法逐渐应用于航空航天等领域的安全关键软件设计与实现中。体系结构分析设计语言(Architecture Analysis and Design Language, AADL)是一种标准化的嵌入式软件体系结构描述语言,通过建模、验证以及代码自动生成为安全关键软件的设计与实现提供完整支持。然而,工业界实际代码是运行在具有不同特性的目标平台上的,例如不同的软硬件体系结构和编程接口,而现有AADL代码生成研究主要是通过手工将自动生成的代码集成到平台当中,存在工作繁琐且易出错的问题。为此,本文提出一种基于AADL的航天嵌入式软件Ada代码自动生成方法。首先,给出卫星姿轨控系统的AADL建模;其次,给出AADL到平台相关的Ada代码自动转化规则;最后,给出代码生成原型工具,并对卫星姿轨控系统AADL模型所生成的代码进行航天编码规范检查,并运行在相关仿真环境中,验证了本文所提方法的有效性。     

AADL模型的形式化研究

在嵌入式系统建模领域,AADL以其软硬件协同建模的特点已经逐渐成为业界的标准。围绕AADL的形式化特点,国内外众多学者展开了热烈的讨论。为了帮助系统开发人员深入了解AADL,指导软件开发进程,提高基于AADL模型的软件开发效率,分别从AADL模型可靠性分析、可调度性分析以及AADL模型测试这三个不同角度综述了已经出现的各种AADL形式化验证理论,对比分析了它们的优点和不足。简要介绍有关AADL验证工具,研究基于AADL模型的嵌入式开发平台的构建。     

AADL建模工具的设计

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

基于SysML & AADL的IMA刹车控制系统实时性需求验证

针对设计阶段难以对刹车控制系统进行实时性分析验证的问题,提出基于SysML & AADL的实时性需求验证方法。首先论述综合模块化航电系统中刹车控制系统的组成和实时性定义,基于SysML建模语言建立系统模型,并添加MARTE描述的组件时间延迟;然后建立SysML/MARTE与AADL的模型元素映射关系,根据该关系,将SysML模型转化为符合AADL语义的模型。最后利用AADL分析工具得到实时性验证结果,验证了所提出实时性验证方法的有效性。     

基于AADL的软件开发技术研究*

形式化方法对于软件的开发过程有着重要的作用。为了研究体系结构分析与设计语言（AADL）在软件开发中的作用及其技术现状,介绍了AADL的语言组成和相关特性,分析了AADL在软件开发过程中的作用,给出了一个相应AADL工具集的框架模型。在此基础上,对现有的AADL相关工具进行了综述比较,总结出该框架的技术现状,并指出了AADL相关工具开发与应用的趋势。     

AADL模型代码自动生成技术研究*

随着嵌入式系统在安全关键领域的广泛应用,必须采用现代软件工程的技术进一步提高其可信性,以保证人们的生命安全。基于模型驱动方法,对AADL（体系结构分析设计语言）模型的框架代码自动生成技术进行了研究,提出了从AADL模型元素到C和Ada的语法元素的映射规则,由此实现了自动代码生成器generator并集成在开源工具OSATE中。最后通过一个实例,说明将AADL模型自动转换为框架代码后与模块代码结合的有效性。     

基于SystemC的AADL软构件仿真代码转换技术

目前,AADL在任务关键和安全关键嵌入式领域有着良好的应用.如何在设计阶段对AADL模型进行仿真,并根据仿真结果迭代构造和精化设计模型,以尽早发现设计模型中存在的问题,保障设计模型的质量,进而减少系统开发的代价,是目前急需解决的技术挑战.SystemC是一种软硬件协同仿真的系统描述语言,由此提出了AADL软构件到Sys...     

AADL模型的测试方法研究

近几年来,MDA开发方式的应用使得如何保证模型质量成为研究的热点.以基于模型的测试为研究对象,研究了对AADL模型进行模型测试的方法,并提出了结合马尔可夫链对AADL模型进行测试的框架以及实施方法.最后,通过示例进一步说明了该方法.     

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

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

AADL进程子集行为语义研究

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

基于XML的UML模型向AADL模型的自动转换

UML已经成为复杂系统建模的工业标准,并可借助代码自动生成工具实现从分析到编码的开发过程自动化;AADL具有精确的语义和严格的语法规范,可用于描述嵌入式实时系统的软、硬件体系结构,并能分析系统的功能及非功能属性。 UML和AADL模型的基本元对象有相互对应关系,并且两种模型的表示都能够采用标准的XML的交换格式。为充分发挥两种语言的优势,文中研究了UML模型向AADL模型的自动转换,以XML为媒介实现两种模型的元对象的对应转换,最终达到两种模型的转换,使用户在设计阶段能够结合运用AADL、UML工具的优点对系统进行分析。     

基于限定自然语言需求模板的AADL模型生成方法

随着嵌入式软件系统在汽车、核工业、航空、航天等安全关键领域的广泛应用,其失效将会导致财产的损失、环境的破坏甚至人员的伤亡,使得保障软件安全性成为系统开发过程中的重要部分.传统的安全性分析方法主要应用在软件的需求分析阶段和设计阶段,然而需求与设计之间的鸿沟却一直是软件工程领域的一大难题.正是由于这一鸿沟的存在,使得需求分析阶段的安全性分析结果难以完整详尽地反映在软件设计中,其根本原因是当前的软件需求主要通过自然语言描述,存在二义性与模糊性,且难以进行自动化处理.为了解决这一问题,本文面向构件化嵌入式软件,首先提出了一种半结构化的限定自然语言需求模板用于需求规约,能够有效降低自然语言需求的二义性与模糊性.然后,为了降低自动化处理的复杂性,采用需求抽象语法图作为中间模型实现基于限定自然语言需求模板规约的软件需求与AADL模型之间的转换,并在此过程中自动记录两者之间的可追踪关系.最后,基于AADL开源工具OSATE对本文所提方法进行了插件实现,并通过航天器导航、制导与控制系统（Guidance,Navigation andControl,GNC）进行了实例性验证.