面向功能行为层次化建模的AADL行为附件扩展及验证方法

发布时间：2020-03-26 20:22

【摘要】：AADL(Architecture Analysis and Design Language)是一种用于描述复杂嵌入式系统体系架构的建模语言国际标准,被广泛用于安全关键系统的建模与验证。AADL通过系统、子系统、进程、线程等组件层次化地表达系统模型。行为附件(Behavior Annex)是AADL在功能行为方面的补充,它通过扁平状态机的形式对组件的内部功能行为以及组件和组件间的交互行为建模。工业界中的复杂系统常使用层次状态机描述组件的功能行为。但是,行为附件中没有表达层次状态机的机制,虽然可以利用AADL自身的分层描述能力对系统建模,但会导致线程的规模过于庞大。在实际的开发过程中,设计者们往往需要将层次化描述的功能需求进行手动扁平化处理,然后借助AADL行为附件对其建模,这个过程是繁琐的且易错的,并且扁平化的状态机会造成结构信息的丢失,无法直观的表示功能行为模块的包含层次关系。针对AADL行为附件不能以层次化的形式建模功能行为这一问题,本文提出了一种基于AADL行为附件的功能行为层次化建模及验证方法,包括基于扩展的AADL层次行为附件建模方法和层次行为附件的形式化验证方法两部分。为了适应工业界的实际建模需求,本文首先提出了AADL行为附件的层次化扩展——层次行为附件HBA,给出了HBA的形式语法,定义了HBA的操作语义,提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了对所建模型进行形式化验证,本文提出了层次行为附件的形式化验证方法。首先通过层次行为附件扁平化方法将层次行为模型转化为多个相关联的扁平状态机,然后通过层次行为附件到时间自动机的转换方法将层次行为模型转换为时间自动机网络,最后人工抽取与被验模型相关属性,并将待验证模型与待验证属性输入到UPPAAL中,对所建模型进行验证。最后,通过一个航天器导航、制导与控制系统案例来验证本文所提方法的有效性。首先通过详细描述建模过程、逐步精化原始需求的方式,检验本文所提建模方法是否适用于建模实际工业案例;然后通过在原始需求中预埋错误的方式,检验本文所提出的HBA形式化验证方法是否可以检测出所建模型与待验证属性存在不一致的问题。
【图文】：

汽艇,自动驾驶仪

第二章基于 AADL 行为附件的功能行为层次化建模及验证方法2.1 AADL 语言及 AADL 行为附件概述2.1.1 AADL 概述为了支持复杂嵌入式实时系统建模与分析，2004 年，美国汽车工程师协会正式发布架构分析与设计语言 AADL。AADL 是一种专为嵌入式实时系统建模而设计的架构描述语言，它支持高度可演化系统的开发，系统架构的早期分析，以及用于整个生命周期持续分析的架构模型的演变。AADL 采用半形式化的建模概念，描述了嵌入式实时系统的软件架构、硬件架构和非功能属性。AADL 通过组件(component)、连接(connection)等概念描述系统的软、硬件体系结构；通过特征(feature)和属性(property)描述系统的功能性质与非功能性质；通过模式变换描述系统运行时体系结构的变化；通过委员会认证的附件(Annex)以及用户自定义的属性集(Property Set)支持扩展；对于建立复杂系统模型，AADL 以包(package)的形式进行分隔与组织[43]。AADL 提供两种建模方式：文本建模与图形化建模，如图 2.1 所示，本文以汽艇自动驾驶仪(PBA)系统 AADL模型为例，介绍 AADL 的基本建模元素。

示例,状态,迁移条件,面向功能

面向功能行为层次化建模的 AADL 行为附件扩展及验证方法位置（状态）没有迁移。位置迁移：由于满足迁移条件而发生的改变。g , a ,ul l ，即满足 g 时，，时的位置（状态）由 l 迁移到了l ，且f I (l )，f I (l )。上述语义，一个时间自动机的迁移过程可以被简化为 l , g , a , u ,l E，其中u U 。图 4.8 给出了一个时间自动机的状态迁移示例，在左图中，gd 为迁移条号（发送）,ud 为迁移更新。右图表示当时钟 cl 大于 10 且接收到同步信号 s从 S3 状态变迁为 S4 状态，同时给变量 x 赋值为 0。
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2019
【分类号】：TP368.1

【相似文献】