AADL综述

精品文档AADL:嵌入式实时系统体系结构设计与分析语言综述 摘要：结构分析和设计语言(architecture analysis and design language)是嵌入式实时系统的一种体系结构描述语言标准，广泛应用于航空宇航工业中对安全关键应用系统模型的建模。本文首先归纳了AADL的发展历程及其主要建模元素。其次，介绍了模型检测方法的研究和应用，并就航电系统与模型检测方法做了研究和分析。最后，探讨了AADL 模型转化为形式化模型，并用模型检测方法进行验证和分析的方法和可行性。 关键字 嵌入式实时系统 AADL 建模 形式化方法 模型验证 1.引言 嵌入式实时系统广泛应用于航空航天、汽车控制、机器人、等安全关键系统领域。由于计算精度、实时响应的要求的提高，系统变得越来越复杂，如何设计与实现具有高可靠性、高质量的复杂嵌入式实时系统，同时有效的控制开发的效率和成本，成为学术界和工业界共同的话题。 模型驱动开发方法(model driven develop- ment，简称MDD)能够在早期阶段对系统进行分析与验证，有助于保证系统的质量属性，并有效控制开发时间与成本。而质量属性是由系统体系结构决定的1。因此，基于体系结构模型驱动(model-based architecture-driven)的设计与开发方法成为复杂嵌入式系统领域的重要研究内容。其中一个重要的方面就是研究合适的体系结构描述语言。 常用的体系结构描述语言主要有UML(unifi- ed modeling language) 和ADL (architecture description language)。UML侧重描述系统的软件体系结构，为了支持嵌入式实时系统的非功能属性分析，OMG(Object Management Group)先后定义了UML Profile for SPT(schedulability， perfor- mance， and time，简称SPT)2，UML Profile for Qos/FT(quality of service and fault tolerance，简称Qos/FT)3以及UML Profile MARTE(modeling and analysis of real-time and embedded sys- tems)4，它们继承了UML 的多模型多分析方法，因此模型之间可能存在不一致性；而C2，Darwin， Wright，Aesop，Unicon，Rapide 等ADL都是通用领域的软件体系结构描述语言，难以满足软硬件协同设计、实时响应、资源受限等特定需求;MetaH 是面向航空电子系统的ADL，可以用于嵌入式实时系统体系结构描述与分析，但MetaH 在支持运行时体系结构描述、可扩展、与其他ADL 兼容以及复杂系统设计等方面有所欠缺。 2004年，SAE(Society of Automotive Engineers)组织在MetaH，UML 的基础上提出嵌入式实时系统体系结构分析与设计标准AADL(Archi- tecture Analysis and Design Language)5。AADL借鉴了UML、MetaH6及多种ADLs的优点，目的是提供一种标准的、足够精确的方式，设计与分析嵌入式实时系统的软件、硬件体系结构及功能与非功能性质，采用单一模型支持多种分析的方式，将系统设计、分析、验证、自动代码生成等关键环节融合于统一框架之下。在嵌入式实时系统领域，还有其他体系结构描述语言：UML profile Marte(Mod- eling and Analysis of Real-Time and Embedded systems，Marte7)是OMG最近提出的嵌入式实时系统体系结构描述语言标准，Marte提供多模型多分析的模式，容易导致各种模型之间的不一致性，且语言本身还不成熟。AADL 具有语法简单、功能强大、可扩展的优点。由于具有广阔的应用景，AADL 得到了欧美工业界，特别是航空航天领域( 例如: Airbus，Lockheed Martin，Rockwell Collins， Honeywell，Boeing)的支持;CMU(Carnegie Mellon University)，MIT(Massachusetts Institute of Technology)， UIUC(University of Illinois at Urbana-Champaign)，Pennsylvania 大学，NASA 以 及法国IRIT(Toulouse Institute of Computer Science Research)，INRIA，Verimag 等研究机构对AADL 展开了深入研究与扩展。 TOPCASED7，SPICES8，AVSI-SAVI9等是欧美工业界和学术界共同参与的AADL 重大研究项目，涉及AADL标准扩展、建模工具、形式语义、验证、可靠性分析、可调度分析以及自动代码生成等方面的研究，这些也是目前AADL的研究热点。 本文的组织结构如下：第二章主要归纳了结构分析和设计语言AADL的主要建模元素；第三章主要介绍了实时系统和航电系统，并总结了模型检测方法在航电系统中的应用；第四章主要介绍了AADL模型可能用到的形式化方法；第五章是结束语部分。 2. AADL简介 2.1 AADL建模元素 AADL描述了系统软件和硬件构件的层次结构，它提供了一组预定义的构件类别，包括： 软件构件:线程，线程组，子程序、数据和过程； 硬件构件:处理器、内存总线，设备、虚拟处理器 和虚拟总线； 系统构件:复合软件构件和硬件构件。 构件由类型和实现构成，构件类型描述构件的外部接口的功能，它可以是端口，服务器子程序或通信范式确定的数据访问；构件实现则描述构件的内部结构，如：子构件、连接、表示构件操作的模式、支持专业架构分析的属性。 1）特征 特征是构件类型定义的一部分，用于描述构件的对外接口，主要包括4类:端口、子程序、参数以及子构件访问。端口用于定义构件之间的数据、事件交互接口，分为数据、事件、数据事件端口。子程序用于定义子程序共享访问接口，分为子程序访问者和子程序提供者，前者表示需要访问其他构件内部的子程序，后者表示提供子程序给其他构件来访问，可以支持远程子程序调用。参数用于定义子程序被访问时输入、输出的合法数据类型。子构件访问分为数据构件访问和总线构件访问，前者用于共享数据或共享资源描述，后者用于硬件平台构件之间的连接。 2）连接 AADL采用连接来描述构件之间的交互行为，与构件特征对应，AADL支持3种连接方式：端口连接、参数连接及访问连接。端口连接用于描述并发执行构件之间的数据与控制交互；参数连接描述一个线程构件访问的所有子程序的参数所形成的数据流；访问连接又分为数据访问连接、总线访问连接以及子程序访问连接，分别描述数据共享、总线共享以及子程序共享。 3）属性 属性用于描述体系结构中的约束条件，即非功能属性约束，进而支持验证与分析系统的可靠性、 安全性、可调度性等性质，如子程序的执行时间、线程的周期、数据或事件端口的等待队列协议、安全层次等。AADL提供了标准的属性集，用户也可以根据需要定义新的属性。属性和特征的区别在于，特征主要是描述构件功能接口，而属性则是描述系统非功能性质的约束。 4）模式 AADL通过模式来描述运行时体系结构的动态演化。模式就是系统或构件的操作状态，如汽车巡航控制系统可能包括初始化、人工控制、自动巡航等模式。它们对应了系统功能行为的不同配置，模式变换体现系统体系结构的变化，能够描述体系结构重构及容错等需求。 5)扩展附件 当定义新的属性不能满足用户需要时，AADL 引入了附件的概念。它拥有独立的语法和语义，但必须与AADL核心标准保持语义一致。如故障模型附件(error model annex)，支持构件、连接的故障事件、故障概率等属性建模；行为附件(behavior annex)增强了AADL对构件实际功能行为的详细描述能力，以更好地支持功能行为验证和自动代码生成。 2.2 AADL形式语义 从数学角度来看，AADL是一种半形式化的建模语言，它只是对系统相应的属性进行了描述。如果要对AADL模型架构的非功能属性进行深入分析，还需要对系统模型的执行通讯进行形式化的验证。AADL的形式化方法就是利用形式化语言的定义来描述AADL，将AADL模型转化为其它的形式化模型，通过已有的形式化工具找出AADL模型中的错误，通过不断修改获得高质量的AADL模型，为开发复杂的嵌入式系统打下基础。 形式化方法能够对语义进行更精确的刻画，有助于体系结构验证与分析。AADL语义从体系结构、执行模型和行为语义三个方面来描述一个系统的模型。采用混成自动机对线程、进程、处理器、虚拟处理器构件的执行状态和动作进行了语义描述，但是AADL并没有形式化定义模式转换、通信、同步/异步访问等执行模型语义，对于系统的一些关键的非功能属性也缺乏严格的论证，主要采用自然语言和例子进行解释。因此，对AADL的语义研究主要针对后面的两项内容。 目前，对于AADL的形式化分析主要采用语义转换的思路来对AADL进行形式化验证，这个方法主要下载文档到电脑，方便使用1下载券 4.9分(高于98.4%的文档)下载 还剩6页未读，继续阅读 定制HR最喜欢的简历我要定制简历 模型转换方法的模型转换语言；Kermeta22是法国INRIA Triskel Team 开发的模型转换语言，能够对元模型的结构、行为进行描述；GreAT(graph rewriting and transformation)23则是一种将图形转换和重写技术应用到模型转换过程中的方法。ATL和Kermeta 在AADL模型转换研究中比较常用。同时，本文认为AADL 模型转换的正确性验证与证明也是需要重点研究的内容。 2.6 AADL模型验证 AADL 的形式化验证就是将AADL 模型降阶转化为其他的形式化工具，通过形式化的方法找出AADL 模型中的错误，然后通过对AADL 模型进行纠正改进，进而获得高可靠性的AADL 模型，为开发大规模复杂、安全可靠的嵌入式系统打下坚实的基础。在国内，目前围绕AADL 模型的形式化研究已经成为了一个热点，针对当前AADL 模型的形式化研究，综述了它们的研究理论和不足，为嵌入式软件的早期开发提供参考。 （1）AADL的可靠性研究 基于AADL 的可靠性分析评估主要通过将AADL 转换成Petrie 网形式化模型，通过一些形式化工具来验证。目前已经有很多学者基于这个思路来分析AADL 模型的可靠性。文献23提出将AADL 嵌入式系统模型转换成可靠性计算模型广义随机网( GSPN) ，基于GSPN 可靠性计算模型对嵌入式系统进行可靠性验证，实现了可靠性分析评估的自动化。并且根据模型转换的形式化方法，设计实现了AADL 的可靠性评估工具AAM( AADL eliability Assessment Model) 。文献24提出了将AADL 模型转换为广义随机网的可靠性验证方法，不过它在已有的基本转换规则的基础上，重点讨论了系统中组件之间错误传播以及系统发生模型转换的Guard _Transition 属性到GSPN 的转换规则，并以飞行控制系统数据发送和处理单元为实例，验证了转换规则和可靠性建模与评估的可靠性。文献25分析了软件内部各种错误状态及其之间的错误传播，构建了AADL 软件系统错误模型，并根据基本的转 换规则将其转换为广义随机网，使用现有的工具对其进行了计算，从而实现了软件容错系统的可靠性评估。文章以航空交通控制系统( ATC)为应用场景进行实验，分析了部分构件的失效率，收到较好的效果。AADL 模型到广义随机网的可靠性计算模型的转换是目前最主要的可靠性评估方式，因为它既 考虑了单个构件的验证，也考虑了构件之间的依赖关系，因此它可以从整体上考虑系统的可靠性。AADL模型可靠性在验证过程需要反复迭代来获取，这可以帮助工程开发人员深入理解系统模型结构和属性。 （2）AADL的可调度性分析 由于嵌入式软件系统对系统的非功能要求非常严格，尤其是系统的响应时间，因此设计基于AADL 模型的嵌入式系统时，如何能够实时快速的响应系统是AADL 可调度性分析的关键。文献26针对AADL 模型的可调度验证问题，提出了利用模型检测工具UPPAAL对其线程组件在非抢占性调度策略下的可调度性进行形式化分析和验证并实现了从AADL 模型到UPPAAL 中模型的模型转换工具。文献27则更进一步实现了AADL 行为模型的分析验证。文章首先基于行为附件的文法结构以及行为描述方式提出了AADL模型与UPPAAL 下时间自动机的模型转换规则。然后在转换规则的基础上，设计和实现了模型转换的原型工具。并以航天器控制中制导、导航与控制计算机从陀螺取数的AADL 模型为例，经自动转换规则得到的自动模型在UPPAAL 下仿真、验证其行为正确性，同时也证明了模型转换的有效性。虽然UPPAAL 是一种良好地分析AADL 模型可调度性的工具，但是在实践中它也有自己的缺点，例如难以描述进行可抢占调度策略下的AADL 模型的可调度验证。文献28则对此进行了补充，它根据AADL 与带约束的时钟自动机理论概念，设计了一种对AADL 模型的可调度性进行验证分析的工具UCaS。并对UCaS 工具的性能进行了测试。不过虽然UCaS 实现了可抢占策略下的AADL 模型的可调度性，但是它的执行效率比较低，稳定性不 够。还需要进一步完善算法，提高执行效率。 在基于AADL 的可调度性上，时间自动机是一种重要的形式化方法。将AADL 降阶转换为时间自动机，利用基于时间自动机的验证工具进行验证是目前的主要方法。在基于AADL 模型可调度性分析上，也有其他一些理论方法。文献29提出了将AADL 模型转换成时间Petri 网的形式化验证方法，并介绍基于时间Petri 网的模型检测工具TINA 的结构。这个工具的工作原理是首先将AADL 模型转换成Fiacre 中间语言，然后将Fiacre 模型用抽象时间自动机编译验证，从而间接验证AADL 模型调度的正确性。这个工具已经作为一个插件被集成在TOPCASED 工具里。以上的基于AADL 模型的分析主 要就是针对AADL 的调度性进行形式化建模，是确保嵌入式系统实时性的关键。 （3）AADL模型测试 目前AADL 已经广泛应用于嵌入式系统领域，如 何保证任务关键软件的质量，还需要给出AADL 的测试模型，对AADL设计模型进行测试。基于这个问题，文献30 31分别提出了基于模型检测的AADL架构验证方法。该方法应用马尔可夫链描述AADL架构的行为，然后根据得到的马尔可夫链模型以及系统设计要求标准生成相应的测试用例和测试语言，并通过测试用例执行输出和期望值的比较判断AADL模型的正确性，实现对系统AADL模型的测试; 最后通过案例分析证明了该方法的有效性。 3. 实时系统概述 3.1实时系统应用背景 二十世纪末，以计算机和通信技术为代表的信息科学与技术在世界经济、军事、教育等领域产生的深刻的影响和变革。从二十世纪六十年代末开始，实时计算（Real-Time computing）已经发展成为一个计算机科学的重要领域。而实时系统作为实时计算的主要载体，其相关技术得到了长足的进步和发展。实时含有立即、及时的意思，所以，对时间的响应是实时系统最关键的因素。目前，实时系统并没有一个统一的定义，但几乎所有的定义都离不开时间性（Timeliness），原因就是实时问题把时间性看作是正确性的判定标准。一般来说，实时系统就是：能及时响应外部发生的随机事件，并以足够快的速度完成对事件处理的计算机应用系统。换句话说，此类系统能及时响应外部事件的请求，在规定的时间内完成事件的处理，并能控制所有实时设备和实时任务协调运行。 与非实时系统相比，实时系统的一个主要特征就是要同时保证逻辑结果和时间的正确性。在实时系统中计算的正确性，不仅取决于逻辑结果的正确，同时还要保证结果在规定的时间内产生，提前或错过规定时间 ，在实时系统中都会看作是不正确的结果。 实时系统已经越来越多的应用于各个领域，包括飞机、太空探测器、火箭控制、舰艇控制、雷达、制导导航等，并且在整个系统中，实时系统通常担负着关键控制系统的角色。 3.2实时系统的研究目的和意义 实时系统是高可靠性计算的典范，同时它又是复杂且带有诸多约束条件的算法集合。因为实时系统自身的这些特点，使其快速发展成为一门系统科学。然而，目前实时系统研究领域，还有很多已知或未知的尚未解决的问题，如：解决系统优先级逆转问题新方法、多处理器单调速率相关算法的可调度性判定问题、具有优先约束的任务调度问题等等。都是当前学术界研究的热点问题。 实时系统任务调度的研究成果对于提高我国国防武器装备、载人航空航天、工业自动控制等领域的关键系统任务调度具有重要的现实意义。上述系统都要求可靠、精确、准时执行预先设定的任务，并要求任务在规定的时间内完成，否则会给系统带来极其严重的后果。 3.3 实时系统的特征 实时系统具有以下的特征： （1）可预测性 所谓可预测性是指系统所执行的操作按预先定义或确定的方式执行，且其执行的时间是可预知的，这是实时系统最重要的特征。可预测性将应用于实时系统环境的每一个组成部分，只有这样，这个环境才能提供一定程度的可预测性。 （2）及时性 实时系统的及时性是非常关键的，主要反映在对用户的响应时间要求上。对于实时系统，对其响应时间的要求类似于分时系统，是由操作者所能接受的等待时间来确定的，通常为秒级。对于实时控制系统，其对时间的响应要求是以控制对象所能接受的延迟来确定的，它可以是秒级，也可能短至毫秒(ms)、微秒级(gs)。当然，响应时间的决定，既依赖于操作系统本身，也依赖于操作系统的宿主机的硬件的处理速度。 （3）交互性 实时系统的交互性根据应用对象的不同和应用要求的不同，对交互操作的方便性和交互操作的权限性有特殊的要求。由于实时系统绝大多数都是专用系统，所以对用户能进行的干预赋予了不同的权限，例如，实时控制系统在某些情况下不允许用户干预而实时信息系统只允许用户在授权范围内访问有关计算机资源。 (4)高可靠性 这是实时系统最重要的设计目标之一。对实时 控制系统，尤其是重大控制项目，如航天航空、核反应、药品与化学反应、武器控制等，任何疏忽都可能导致灾难性后果，必须考虑系统的容错机制。对实时信息系统，则要求数据与信息的完整性，要求经过计算机处理、查询并提供给用户的信息是及时的、有效的、完整的和可用的。 (5)多路性 实时系统也具有多路性。实时控制系统常具有现场多路采集、处理和控制执行机构的功能，实时信息系统则允许多个终端用户(或者远程终端用户)向系统提