免费论文摘要：AADL情势语义及安定要害及时体例考证与领会接洽

安定要害及时体例普遍运用于宇航电子、航天器、兵戈装置、核能、公共汽车遏制等要害消息范围。因为功效和非功效诉求连接普及，体例的搀杂度急遽减少，怎样安排与实行高品质的安定要害及时体例，并灵验遏制开拓功夫和本钱，是学术界和产业界共通面对的困难。连年来，模子启动开拓本领渐渐变成安定要害及时体例安排与开拓的要害本领，而动作搀杂嵌入式及时体例的体制构造安排与领会谈话规范，AADL(Architecture Analysis and Design Language)日益遭到关心，并渐渐兴盛变成一个新的接洽热门。 AADL谈话供给了一种规范、所有的办法，对安定要害及时体例的软/硬件体制构造、运转时情况、功效以及非功效属性举行表白，而对AADL模子举行情势考证与领会是实行高确凿安定要害及时体例的一个要害步骤。正文的处事恰是环绕这一要害接洽题目打开的。暂时，模子变换是AADL模子情势考证与领会的重要道路，如变换到BIP(Behavior Interaction Priority)、Fiacre、举措时序论理TLA+、同步谈话等，手段是为了重用那些情势模子上已有的考证和领会本领。但是，其要害题目在乎：(1) 对AADL规范设置的语义能否有明显和精确的领会，这是AADL模子变换的普通，但是，AADL大局部语义利害情势化的；(2) AADL模子变换能否精确或灵验，即AADL语义在模子变换中能否获得维持；(3) AADL模子上满意的考证本质，在目的模子上能否也满意，反之亦然，即用户憧憬考证的本质在模子变换中能否获得维持。 正文提出了一种新的AADL模子情势考证与领会本领，中心接洽了AADL情势变换语义、AADL模子变换的语义维持表明本领以及AADL模子变换的考证本质维持表明本领三个要害题目，并安排和开拓了一体化的AADL建立模型与考证平台。重要接洽功效如次： (1)对准“大局部AADL变换语义接洽不够完备和情势化，且较少关心资源动作的表白”的题目，提出了一种鉴于功夫笼统状况机(Timed Abstract State Machine, TASM)的AADL情势变换语义框架－AADL2TASM。对准一个较为完备的AADL接洽子集，给出了接洽子集的情势设置和笼统语法，给出了TASM的笼统语法及其操纵语义，并鉴于语义因变量和类ML的元谈话情势设置变换语义准则。与已有AADL变换语义接洽比拟，该框架具备较为完备的AADL接洽子集、较强的目的谈话表白本领以及对东西谈话、目的谈话和变换语义准则透彻刻画等便宜。 (2)对准“已有AADL模子变换较少举行语义维持表明”的题目，提出了一种鉴于双本子情势语义的AADL模子变换的语义维持表明本领－ASemPre。给出了功夫变化体例(Timed Transition System, TTS)及其操纵的设置；和情势变换语义对应，鉴于TTS以操纵语义的办法给出了相映AADL接洽子集的语义，动作语义维持表明的一个基础，同声，将变换语义设置中的TASM表白和TASM谈话自己的操纵语义举行拉拢，形成TTS，动作语义维持表明的另一个基础，结果，证领会两个TTS满意模仿等价联系(Simulation Equivalence)，即AADL接洽子集的语义在AADL到TASM的模子变换中获得维持，为了普及表明的确凿度，鉴于定理证冥器Coq对关系定理举行了表明。该本领克复了已有AADL模子变换接洽中仅沿用细工确认大概假如语义是维持的缺陷，从表面上证领会AADL接洽子集的语义在AADL到TASM的模子变换中获得维持。 (3)对准“已有AADL模子考证与领会本领较少举行考证本质维持表明”的题目，提出了AADL模子到TASM模子的考证本质维持表明本领－AVerPre。给出了商量亚原子命题的功夫变化体例及其操纵的设置；给出了时序论理ACTL、ECTL的语法和语义；给出了一种比拟通用的考证本质维持的表明思绪，其要害在乎亚原子命题、亚原子命题的满意联系和亚原子命题的映照联系的设置以及亚原子命题满意联系维持的表明，鉴于构造归结法，进而所有本质获得维持。表明截止表白，正文提出的AADL到TASM的模子变换满意模仿等价联系，且亚原子命题的满意联系获得维持，所以，运用时序论理ACTLUECTL表白的无死锁性、安定性、活性、及时本质以及资源本质不妨获得维持。同声，鉴于定理证冥器Coq对关系定理举行了表明。 (4)在上述表面处事的普通上，安排并实行了AADL建立模型与考证平台－CertA2T，同声，鉴于航天器导航、制导与遏制体例(Guidance, Navigation and Control, GNC)举行了范例性考证，因为GNC体例特殊搀杂，提出了分层建立模型本领，囊括体例与子体例层、工作层和动作层三个档次，而且精细计划了怎样运用CertA2T平台对AADL模子举行考证和领会。

来源：半壳优胜育转载请保留出处和链接！

本文链接：http://www.87cpy.com/200273.html