马燕燕,杨志斌,2,江国华
(1.南京航空航天大学计算机科学与技术学院,江苏 南京 211106; 2.高安全系统的软件开发与验证技术工信部重点实验室,江苏 南京 211106)
安全关键系统(Safety-Critical System)是其故障可能导致生命损失、重大财产损失或环境破坏的系统,广泛应用于航空、航天、交通和能源等领域。随着安全关键系统规模和复杂性不断提高,这类系统出现错误的可能性及其造成的危害也日益突出。2019年3月10号,埃及航空的一架波音737MAX8客机在从埃塞俄比亚首都飞往肯尼亚首都内罗毕途中失事,机上157名乘客无人生还。失事的主要原因是由于高迎角传感器将错误的数据输入给飞行控制系统,从而引起错误的机头降低指令,使得驾驶员难以判断和控制飞行状态造成的。
安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。设计阶段首先进行系统设计,然后区分软硬件,进行软件和硬件协同设计。近年来,模型驱动(Model-Driven)尤其是采用形式化模型驱动的安全关键系统设计与开发方法逐渐受到重视,并被工业界认为是保障系统安全性与可靠性切实可行的重要手段。基于模型的系统工程(Model-Based Systems Engineering)支持从概念设计阶段开始并在整个开发生命周期阶段中持续进行的系统需求、设计、分析、验证和确认活动。侧重于利用领域模型作为工程师之间信息交换的载体,而不是基于文档的信息交换[1]。
安全关键领域常用的建模语言有UML(Unified Modeling Language)、SysML (Systems Modeling Language)[2]、航空电子系统描述语言MetaH和HOOD(Hierarchical Object Oriented Design)、汽车电子系统描述语言EAST-ADL(Electronics Architecture and Software Technology-Architecture Description Language)、嵌入式实时系统体系结构分析与设计语言AADL(Architecture Analysis & Design Language)[3]等。然而,目前还没有一个标准的建模语言支持安全关键系统的整个开发生命周期。因此,考虑集成使用适合于系统设计阶段建模的SysML和适合于软硬件协同建模的AADL。SysML适合于进行需求捕获、分析和初步系统设计,而AADL适合于详细设计阶段,区分软硬件,可采用仿真和形式化方法进行模型的验证与分析。
目前,SysML和AADL的集成使用已经成为一个研究热点。例如,挪威奥斯陆大学Simula研究所[4,5]提出了ExSAM概要文件(Profile)的概念,它通过向SysML添加AADL概念来扩展SysML,能够对系统工程概念建模,并在需要时使用AADL分析工具。图卢兹大学的de Saqui-Sannes等人[6]提出了一种基于模型的安全关键嵌入式系统设计、验证和实现方法,将标准化的SysML和AADL结合在一起,用于系统级建模、需求捕获、用例和场景分析、体系结构描述,并使用SysML和AADL对飞行管理系统进行无缝建模、验证和实现。进一步地,Wang等人[7]提出在整个模型驱动工程中集成使用SysML、AADL和FACE (Future Airborne Capability Environment);在工业界,ANSYS公司提供SCADE System用于SysML系统模型设计,提供SCADE Suite用于软件设计,SCADE System和SCADE Suite可进行无缝对接。在SCADE System中定义的模块接口能自动转换到SCADE Suite中的接口,并且在两者中保持同步[8]。
在这些已有研究中,挪威奥斯陆大学Simula研究所[4,5]将AADL核心元素扩展到SysML中用以区分软硬件,但是无法与AADL分析工具无缝对接,分析时仍需手工完成SysML模型到AADL模型的转换。图卢兹大学的de Saqui-Sannes等人[6]提出将SysML状态机图转换为AADL行为附件,状态机图较难描述输入通过一系列动作转换为输出的过程。另外,SCADE只支持System的BDD(Block Definition Diagram)、IDB(Internal Block Diagram)向AADL模型的转换。
本文提出一种SysML模型到AADL模型的自动转换方法。首先定义SysML子集SubSysML,SubSysML包括BDD、IBD、ACT子集以及在IBD和BDD上扩展的AADL Profile;其次提出SubSysML模型向AADL模型转换的具体规则,并且设计基于Eclipse的模型转换工具SubSysML2AADL,实现SubSysML向AADL模型自动转换,通过模型来自动传递设计信息;由于SysML和AADL在不同的抽象层次进行建模,因此在获得AADL初始模型之后,通过求精的方式将一些设计细节增加到AADL模型中;最后通过工业界案例雷达信息处理系统验证本文方法的有效性。
本文第2节介绍SysML语言和AADL语言;第3节介绍SysML模型到AADL模型的转换方法总体研究框架;第4节定义SysML子集SubSysML;第5节描述SubSysML到AADL的转换方法;第6节介绍SubSysML到AADL的模型转换工具实现;第7节以典型工业应用案例说明本文方法的有效性;第8节对国内外的相关研究工作进行相应概述;第9节对研究工作进行总结和展望。
本节主要介绍SysML和AADL的基本建模概念。
国际系统工程学会INCOSE(International Council on Systems Engineering)和对象管理组织 OMG(Object Management Group) 在对 UML2.0 的子集进行重用和扩展的基础上,提出一种新的系统建模语言——SysML,作为系统工程的标准建模语言[9]。SysML是一种通用的图形建模语言,旨在帮助指定和构建系统,并指定可以使用其他特定于领域的语言设计的组件。SysML中定义了9个图来描述系统。
(1)描述需求。
需求图用于表示基于文字的基本需求、需求之间的关系以及满足、验证和改善它们的其他模型元素。
(2)描述结构。
①模块定义图BDD表示模块和值类型之类的元素。
②内部模块图IBD用于指定单个模块的内部结构。
③参数图用于表示1种或多种约束如何与系统的属性绑定。
④包图用于显示模型以包相互包含的层级关系形式组织的方式。
(3)描述行为。
①用例图从系统参与者的角度表达系统执行的用例,是一种黑盒视图。
②活动图ACT(Activity Diagram)用于指定一种行为,主要关注控制流程,以及输入通过一系列动作转换为输出的过程。
③序列图用于指定一种行为,主要关注模块的组成部分如何通过操作调用和异步信号交互。
④状态机图用于指定一种行为,主要关注模块的一系列状态,以及响应事件时状态之间的转换。
关于 SysML 的扩展机制,官方主要提供了如下3个途径[2]:基于 UML构造型(Stereotypes)、基于 UML
图元扩展(Diagram extensions)和基于模型库(Model libraries)。SysML 构造型机制通过用新的属性和约束来扩展现有的 UML2.0构造型,从而定义新的建模元素;SysML
图元扩展通过定义新的图元符号,用于补充从 UML2.0中重用的图元符号;SysML 模型库则用于描述可供重用的专用模型元素。
2004 年,美国汽车工程师协会SAE (Society of Automotive Engineers)在MetaH、UML等建模语言的基础上,提出了嵌入式实时系统体系结构分析与设计语言AADL[3],目的是提供一种标准而又足够精确的方式,设计与分析嵌入式实时系统的软、硬件体系结构及功能与非功能性质,采用单一模型支持多种分析的方式,将系统设计、分析、验证、自动代码生成等关键环节融合于统一框架之下[10]。AADL的这些特性使其具有广阔的应用前景,得到了以航空航天领域(如空客、波音、霍尼韦尔等)为首的欧美工业界的支持,此外学术界也对AADL展开了深入的研究和扩展,其中,美国卡耐基·梅隆大学开发的开源AADL集成开发环境OSATE(Open Source AAOL Tool Environment)已被广泛使用。
安全关键系统是应用软件、运行时环境以及硬件平台深度融合的复杂系统,AADL语言与之对应地提供了软件体系结构、运行时环境以及硬件体系结构的建模概念[10]。AADL 提供了一组预定义的构件类别:
(1)软件构件:包括线程、线程组、子程序、数据和进程。
(2)执行平台构件:包括处理器、内存、总线和外设。
(3)系统构件:用系统表示软件和执行平台的组合集。
为了支持组件内部的控制流建模,法国图卢兹计算机与信息研究所IRIT(Institute de Recherche en Informatique de Toulouse)[11]实验室于 2006 年提出了 AADL 行为附件BA(Behavior Annex)。行为附件以变迁系统(Transition System)的形式增强了 AADL 线程构件和子程序构件功能行为的详细描述能力。行为附件与执行模型有密切的关系:执行模型定义行为附件何时执行、哪些数据被改变,而行为附件处于构件内部,对线程、子程序构件的执行给予更精确的描述。行为附件是执行模型调度机制的扩展,用于更精确地描述模型行为,例如端口通信、子程序调用、时序、异步等。完整的 AADL 模型应该包括执行模型和行为附件。
行为附件主要包括3部分:变量、状态和转换。变量部分声明当前行为附件中使用的所有局部变量。局部变量可以用来保存当前行为附件范围内的中间结果。状态部分枚举状态机的所有状态及其属性(initial,complete,final或它们的组合)。默认状态是一个执行状态。转换定义了从源状态到目标状态的转换,转换可以有条件和动作。
SysML模型到AADL模型的转换方法总体框架如图1所示,整个过程分为3个部分:
(1)定义SysML子集SubSysML,包括IBD子集、BDD子集、从IBD和BDD扩展的AADL Profile,以及ACT的子集。
(2)定义SubSysML到AADL转换规则以及具体的转换算法,生成AADL初始设计模型。
(3)对第(2)步生成的AADL初始设计模型使用同步语言Signal进行精化。针对不同应用,对AADL初始设计模型可以使用BA、Signal、SDL(Specification and Description Language)进行功能行为求精设计。BA是AADL的标准扩展,支持以自动机的方式表达控制流形式的功能行为;而同步语言Signal则是基于数据等式的方式表达(同步)数据流形式的功能行为,例如用数学公式所表达的应用功能往往可以通过同步语言来建模;SDL则是一种接近常用C程序的数据流和控制流表达语言,其语义为异步执行,接近我们常用的执行程序。本文主要使用Signal对功能设计进行精化。
Figure 1 Framework of model transformation from SysML to AADL图1 SysML到AADL的模型转换方法研究框架
SubSysML包括BDD子集SubBDD、IBD子集SubIBD、对BDD中的Block和IBD中的FlowPort扩展得到的AADL Profile,以及ACT子集SubACT。其定义如下:
定义1SubSysML = 〈SubBDD,SubIBD,SubACT,AADL Profile〉,其中:
SubBDD ={Block,Realization},Block为SysML结构中的基本单元,可以使用模块为系统中或者系统外部环境中任意一种实体类型创建模型,Realization为系统声明的Block和系统实现的Block之间的实现关系。
SubIBD={Block,Part,FlowPort,Connector},Block为SysML结构中的基本单元;Part为Block的组成部分;FlowPort为端口,代表结构边缘不同交互点的一种属性;Connector为2个Part之间的连接器。
AADL Profile={system,data,eventPort,dataPort,eventDataPort,dataAccess},system表示该Block 表示一个系统,data表示该Blcok为数据组件,eventPort表示该FlowPort为事件端口,dataPort表示该FlowPort为数据端口,eventData-Port表示该FlowPort为事件数据端口,dataAccess表示数据组件上的端口。
SubACT={ActivityNode,ActivityEdge,Variable},ActivityNode为活动图的节点,ActivityEdge为活动图的边,Variable为活动图中需要使用的局部变量。
AADL Profile是对SysML描述能力的补充。本文使用构造型的方式扩展SysML。AADL Profile如图2所示。首先定义扩展自SysML Block 构造型的2个新的构造型 system 和data,用于区分Block代表的是系统还是数据组件,SysML Block 扩展自UML的类,并被选择为组件建模,在使用时添加system构造型表示该Block表示为系统,添加data构造型自定义复杂数据类型。其次定义新的构造型dataPort、eventDataPort和eventPort分别表示数据端口、事件数据端口和事件端口,dataAccess扩展自SysML FlowPort构造型,表示数据组件上的端口。
图3所示为SysML活动图子集SubACT元模型,包括活动节点(ActicityNode)和活动边(ActivityEdge)2个部分,定义如下:
定义2ActicityNode = 〈ExecutableNode,ControlNode,ObjectNode〉,其中:
ExecutableNode={SendSignalAction,AcceptEventAction,CallBehaviorAction},SendSignalAction为发送信号动作,AcceptEventAction为接收事件动作,CallBehaviorAction为调用行为动作,在启动时触发另一种行为。
Figure 2 AADL profile图2 AADL 概要文件
Figure 3 Meta model of SubACT图3 SubACT元模型
ControlNode={InitialNode,DecisionNode,MergeNode,ForkNode,JoinNode,FinalNode},InitialNode为初始节点,标记活动的起点;DecisionNode为决定节点,标记活动中可替换序列的开始;MergeNode为合并节点,标记活动中可选序列的结尾;ForkNode为分支节点,标记活动中并发序列的开始;JoinNode为集合节点,标记活动中并发序列的结束;FinalNode为终止节点,标记控制流的结束。
ObjectNode={InputPin,OutputPin},其中InputPin表示动作的输入数据,OutputPin表示动作的输出数据。
定义3AcitivityEdge = 〈ObjectFlow,ControlFlow〉,其中ObjectFlow为对象流,表示事件,数据的实例通过活动从一个节点向另一个节点流动;ControlFlow为控制流,表示可以传递控制令牌的边,控制令牌的到达可以启动等待它的动作。
从SysML模型到AADL模型的自动转换主要包括2部分:
(1)系统基本结构的转换。系统的基本结构即SubIBD、SubBDD中的元素,以及扩展的AADL Profile,将其对应转换为AADL体系结构模型。例如Block对应转换为Component构件,根据Stereotype的不同,system Stereotype对应转换为system构件,data Stereotype对应转换为data构件。
(2)系统行为的转换。系统行为涉及到的元素主要为SubACT中的元素。活动图对应转换为AADL 模型的行为附件。一个system Stereotype的活动图对应拆分为该system Stereotype对应的system构件的subComponent的行为附件。
系统基本结构的转换规则如下所示:
(1) Rule1:SysML模型中的Package元素转换为AADL模型的Package构件。
(2) Rule2:SysML模型中的模块定义图中使用system Stereotype的Block元素转换为AADL的system构件。若2个Block之间存在Realization关系,则supplier端的Block转换为system Type构件,client端的Block转换为system Implementation 构件。若同时使用data构造型,则对应转换为AADL的数据构件。
(3) Rule3:SysML模型中Block的内部模块图Part 元素转换为对应AADL模型中system的subComponent构件。
(4) Rule4:SysML模型中Block的内部模块图Connector元素转换为AADL模型 的connection构件。
(5) Rule5:SysML模型中Block的内部模块图Port元素转换为AADL模型中feature的port。Port元素若同时使用dataPort 构造型,则转换为 dataPort端口;若同时使用dataEventPort 构造型,则转换为 dataEventPort端口;若同时使用eventPort 构造型,则转换为 eventPort端口。
系统行为的转换规则如下所示:
(1) Rule1:SysML模型中Block的活动图转换为AADL模型对应的system构件的子组件的行为附件。
(2) Rule2:活动图中一个InitialNode转换为对应AADL模型中行为附件中的initialstate。
(3) Rule3:活动图中的action转换为AADL模型对应行为附件中的transition语句中的behavior_action_block。其中SendSignalAction转换为行为附件的Transition中的发送语句port!(var)。AcceptEventAction转换为行为附件的condition中的on dispatch port。并且为接受事件对应的状态添加complete标识。CallBehaviorAction转换为子程序调用。活动图中的元素通过分配表明确活动节点的动作和Block的分配关系。
(4) Rule4:活动图中的局部变量转换为AADL模型对应行为附件中的variables。
(5) Rule5:活动图中的ActivityEdge转换为AADL模型对应行为附件中的state。
(6) Rule6:活动图中的DecisionNode中的guard转换为AADL模型对应行为附件中transition中的behavior_ condition。
(7) Rule7:活动图中的FinalNode转换为AADL模型对应行为附件中的FinalState。
基于SubSysML和AADL元模型,本文给出SubSysML到AADL的转换算法,如算法1所示。
Algorithm1Transformation from SysML to AADL
Input:SysML_ModelS。
Output:AADL_ModelM。
01:for each BlockbinS.getBlocksdo
02: ifb.isSystemthen
03:M.add(new Systemn);
04: else ifb.isDatathen
05:M.add(new Datan);
06: else
07:M.add(new Abstractn);
08: end if
09:M.addInstance(n.newInstance);
10:b.getPorts→n.features;
11:b.Parts→n.instance.subcomponents;
12:b.Connector→n.instance.connections;
13:b.Activity→n.instance.subcomponents.BA;
14: for each Elementeinb.Activitydo
15: ife.isVariablethen
16:BA.add(new Variablev);
17: else ife.isInitialStatethen
18:BA.add(new InitialStates);
19: else ife.isActivityEdgesthen
20:BA.add(new States);
21: else ife.isActionthen
22:BA.add(new Transition.behavior_
23: action_blocka);
24: else ife.isDecisionNodethen
25:BA.add(new Transition. Behavior
26: _conditiong);
27: elsee.isFinalNodethen
28:BA.add(new FinalStatef);
29: end if
30: end for
31:end for
Figure 4 Framework of SubSysML2AADL tool图4 SubSysML2AADL工具框架
本文在已经集成OSATE和Papyrus插件的Eclipse平台上进行SubSysML2AADL工具的开发。Papyrus是一个工业级的基于开源模型的工程工具。Papyrus为SysML提供了完整的支持,以支持基于模型的系统工程。还提供了SysML所需的特定表格和图形编辑器。OSATE用于AADL建模、编译和分析,以及进行可调度性分析和安全性分析和时间延迟分析等。SubSysML2AADL是基于EMF(Eclipse Modeling Framework)框架实现的。EMF是一个建模框架和代码生成工具,用于构建基于结构化数据模型的工具和其他应用程序。使用EMF设计满足SubSysML语法的Ecore元模型,为模型生成1组Java类,进而通过编写转换规则实现向AADL的转换。SubSysML2AADL工具框架如图4所示。
首先分析存储SysML模型的XML文件,定义1个EMF元模型,用于描述XML文件的元结构,所述EMF元模型可自动生成框架代码,复用该框架代码可生成SysML模型解析器并通过EMF提供的API读取XML文件的信息,生成EMF对象。其次根据制定的SubSysML到AADL的关系对应,对从SysML模型中读取的EMF对象,使用OSATE提供的API生成对应的AADL对象。最后使用AADL和EMF对象之间的映射以及EMF对象之间的关系来填充AADL对象之间的链接,完成AADL初始设计模型的生成。
雷达信息处理系统主要应用于空中监视、空间和导弹监视、表面搜索和战场监视、跟踪和制导、气象雷达、天文和大地测量。雷达是利用目标对电磁波反射现象来发现目标并测定其位置的。雷达信息处理系统一般由天线、前端处理和后端处理3部分组成。前端主要做A/D采样、下变频和脉冲压缩,后端主要做成像和匹配定位。其中后端主要包括成像模块和匹配模块2部分,成像模块由2个DSP和1个FPGA构成,匹配模块由2个DSP和2个FPGA构成。雷达信息处理系统的抽象结构如图5所示。
Figure 5 Framework of radar information processing system图5 雷达信息处理系统抽象框架图
Figure 6 BDD of radar information processing system图6 雷达信息处理系统的BDD
使用Papyrus对雷达信息处理系统进行建模,建立BDD描述雷达信息处理系统功能模块之间的组成关系,建立IBD对BDD的内容做补充,描述单个模块内部组成部分之间的数据连接。成像和匹配是雷达最重要的2个功能模块,本文选择成像模块建立活动图描述成像的执行过程。表1所示为该雷达模型的数据统计。图6所示为雷达信息处理系统的BDD。
Table 1 Statistical data of SysML model of radar information processing system表1 雷达信息处理系统的SysML模型数据统计
图7所示为成像模块Main DSP活动图,当Main DSP收到开始扫描指令后,解析指令,获得指定的高度Height,然后判断高度,根据高度的不同取值进入不同的模式。当1 Figure 7 Activity of Main DSP of the imaging module图7 成像模块Main DSP活动图 完成雷达信息处理系统的SysML建模后,通过SubSysML2AADL工具,可以将SysML模型转换成AADL初始设计模型。模块定义图和内部模块图表示的系统结构自动转换为AADL体系结构模型,活动图表示的系统行为自动转换为AADL模型中对应构件的行为附件。图8所示为生成的Main DSP模块的AADL模型图形化表示。由图7的SysML活动图生成的AADL行为附件如下所示: annexbehavior_specification{** variables startScanOrder_variable: Data_Types::startScanOrder.Impl; DetectHeightPulseData_variable: Data_Types::DetectHeightPulseData.Impl; PrtInterrupt_variable: Data_Types::PrtInterrupt.Impl; DetectHeightRelevantParameter_variable: Data_Types:: DetectHeightRelevantParameter.Impl; pluseWidthAndBandWidth_variable: Data_Types::pluseWidthAndBandWidth.Impl; states s0:initial state; s1:complete state; s2:state; s3:state; s4:state; s5:state; s6:state; transitions t0:s0-[]→s1{count0:=0;count1:=0; num1:=7;num2:=4}; t1:s1-[on dispatchstartScanOrder]→s2{ startScanOrder?(startScanOrder_variable); t2:s2-[]→s3{calculatedAltitude!}; t3:s3-[(2 and(startScanOrder_variable.height<3)] →s4{calculatingParameter!}; t4:s4-[]→s5{pluseWidthAndBandWidth! (pluseWidthAndBandWidth_variable)}; t5:s5-[]→s6{calculatingfilterCoefficient!}; SysML主要关注系统级建模,在对雷达信息处理系统进行系统级建模时,对于计算过程,在活动图中使用CallBehaviorAction元素来描述,通过CallBehaviorAction的name表达计算的含义,没有对具体的计算过程进行建模,所以对应生成的AADL模型中的子程序都是空的。以子程序calculatingParameter为例,本文介绍同步语言的人工求精过程。calculatingParameter子程序主要完成多普勒中心估计的计算过程,在进行双侧扇扫前,由于不同方向的回波具有不同的多普勒值,需要估计多普勒中心。使用同步语言估计多普勒中心过程如下所示: Figure 8 AADL model of Main DSP module图8 Main DSP模块的AADL模型 01: processDoppeParameterEstimation:= 02: (! realnrn,nan; 03: ? realf′ 04: ) 05: (|R11:=F11(nrn,nan) 06: |… 07: |R14:=F14 (nrn,nan) 08: |K1:=F21(R11) 09: |… 10: |K4:=F24(R14) 11: |K′:=F3(K1,…,K4) 12: |f:=F4(K′) 13: |) 14: where 15: realR11,R12,R13,R14,K1,…,K4,K′; 16: end 其中,第2~4行输入输出信息,第5~7行计算4个符号相关参数,第8~10行导出相应的相关系数,第11行导出复数相关系数,第12行将幅角转变为多普勒中心频率。在calculatingParameter子程序中调用该同步语言过程来估计多普勒中心。 在SysML的建模和扩展方面,挪威奥斯陆大学Simula研究所Behjati等人[4,5]提出了ExSAM(Extended SysML for Architecture Analysis Modeling)概要文件,它通过向SysML添加AADL概念来扩展SysML,能够对系统工程概念建模,并在需要时使用AADL分析工具。但是,使用AADL的分析工具的前提是手工将ExSAM的建模片段转换为AADL模型。Ribeiro等人[12]探讨了UML、SysML和实时及嵌入式系统建模与分析语言MARTE(Modeling and Analysis of Real Time and Embedded system)在RTS的软硬件需求建模中的结合使用,表明仅SysML无法精确表达时间和性能方面的需求。由于SysML 可以通过建立不同的模型,从多个角度反映整个系统的结构特征,褚长勇等人[1]提出SysML需求图到用例图、用例图到序列图的转换,从而提高了建模效率。李路野等人[13]以雷达信号处理系统为研究背景,提出了一种模型驱动的软件开发流程,使用SysML建模并自动生成C代码框架。 在SysML和AADL的集成使用研究方面,图卢兹大学的de Saqui-Sannes等人[6]提出了一种基于模型的安全关键嵌入式系统设计、验证和实现方法,将标准化的SysML(包括AVATAR实时概要文件)和AADL结合在一起,用于系统级建模、需求捕获、用例和场景分析、体系结构描述,并使用SysML和AADL对飞行管理系统进行无缝建模、验证和实现。Wang等人[7]研究了在基于多模型驱动工程中,如何有效集成使用SysML、AADL和FACE,从而涵盖从早期的需求捕获到最终的系统和嵌入式软件的生成。万小平等人[14]研究了基于XML的UML向AADL的模型转换,使用户在设计阶段能够结合运用AADL和UML工具的优点对系统进行分析。本文关注SysML,是因为SysML可通过可跟踪需求和通用的Block等特性支持系统工程。邓佳佳等人[15]提出了一种SysML & AADL 的航电刹车控制系统实时性需求验证方法,基于 SysML 建模语言建立系统模型,并在状态机图上添加用MARTE 描述的组件时间延迟,将SysML 模型转化为符合 AADL 语义的模型。最后利用 AADL 分析工具得到实时性验证结果。 本文提出一种SysML模型到AADL模型的自动转换方法。首先定义SysML子集SubSysML;然后定义SubSysML到AADL的转换规则及转换算法,使用EMF框架技术实现SubSysML模型到AADL模型的自动转换,对生成的AADL初始设计模型使用同步语言进行精化;最后以雷达信息处理系统为案例验证了本文方法的有效性。 在SysML模型转换为AADL模型的过程中,如果目标模型与源模型语义不一致,即使源模型能够满足系统设计要求,也无法保证转换后的目标模型也满足相应的性质,出现了语义保持(Semantics Preservation)问题。语义保持问题是模型转换过程中的重要研究内容,其证明大致可以在2个层次展开:模型实例层次(Instance-based)和语言层次(Language-based)。前者针对具体的模型实例,每次转换都需要重新证明,通用性不够;后者针对源语言和对象语言的所有语法结构及语义,只需证明1次就可以推广到任意模型实例,但证明难度较大。未来,计划研究基于时间变迁系统的互模拟等价(Bi-simulation)、单向模拟(Simulation)等价的基本方法,并基于定理证明器Coq对模型转换的语义一致性保持进行证明。7.3 AADL模型的生成
8 相关工作
9 结束语