模型驱动的嵌入式系统设计安全性验证方法研究*
2015-09-22黄志球马金晶石娇洁
刘 雪，胡 军，2，黄志球，马金晶，程 桢，石娇洁
（1.南京航空航天大学计算机科学与技术学院，江苏 南京 210016；
2.南京大学计算机软件新技术国家重点实验室，江苏 南京 210093）
模型驱动的嵌入式系统设计安全性验证方法研究*
刘 雪1，胡 军1，2，黄志球1，马金晶1，程 桢1，石娇洁1
（1.南京航空航天大学计算机科学与技术学院，江苏 南京 210016；
2.南京大学计算机软件新技术国家重点实验室，江苏 南京 210093）
基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向Sys ML/MARTE状态机的系统安全性验证方法，具体包括：构建了具备Sys ML/MARTE扩展语义的状态机元模型，以及安全性建模与分析语言AltaRica的语义模型GTS的元模型；然后建立了从Sys ML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则，并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对Sys ML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。
系统安全性分析；模型驱动工程；Sys ML/MARTE；状态机模型；嵌入式系统
1 引言
模型驱动工程MDE（Model Driven Engineering）［1～3］是近十年来在系统工程 以及软件工程领域中出现的主流方法，其基本思想是以系统模型设计、模型转换与分析/验证为工程的重要核心，提高对复杂工程系统开发与维护的能力和效率。与此同时，建立基于模型的系统安全性分析方法并结合形式化方法进行验证也逐渐成为嵌入式安全攸关系统开发过程中的需求和重要挑战，如：在2013年版本的机载软件安全性适航标准DO-178C中已经正式提出了基于模型的系统开发和形式化方法分析 的要求［4］。
传统的嵌入式系统设计与开发中是由安全工程师来直接构造故障树、马尔科夫链等进行系统安全性分析，不足以应对近年来规模和复杂度迅速增长的嵌入式安全攸关系统的设计开发与升级维护的要求，需要在系统设计开发过程中尽可能采用统一的模型形式，建立有效的系统模型转换方法并结合形式化分析技术来提高系统安全性分析的效率［5，6］。Sys ML（System Modeling Language）［7］是目前系统工程应用开发的标准建模语言规范，支持包括对复杂嵌入式系统进行规约、设计和分析。MARTE（Modeling and Analysis of Real-Time Embedded systems）［8］主要提供了嵌入式系统中的时间约束、资源分配等非功能属性的建模与分析。通常这两者结合起来可以有效描述嵌入式实时系统的功能行为。AltaRica［9］是一个以卫式转换系统为语义基础进行系统安全行为建模与分析的语言及工具，已在航空电子设备系统架构安全评估 中得到 应 用［10］。
本文的主要研究工作是在 MDE架构下以Sys ML模型中的状态机模型作为核心研究对象，结合MARTE中的时间、资源等方面语义扩展，用以对复杂嵌入式实时系统的行为建模；然后分别建立从Sys ML/MARTE状态机模型到AltaRica模型的转换和Sys ML/MARTE状态机模型到时间自动机模型的转换方法，并在AMMA（ATLAS Model Management Architecture）［11］平台上进行了包括语法/语义的模型转换的具体实现。前者的转换使我们能在AltaRica模型中获取安全性分析所需要的故障树以及相应的时序逻辑公式；后者的转换使得可以采用形式化分析工具UPPAAL来展开系统行为设计的安全性验证。
具体内容安排如 下：第 2节概 要介绍了Sys ML及MARTE模型，并针对Sys ML中的状态机模型，给出了在本文工作中所构造的结合MARTE语义信息的扩展状态机的元模型；第3节主要介绍了AltaRica安全性建模语言及其形式化描述GTS模型；第4节给出了本文所提出的基于模型转换的安全性验证框架，包括从Sys ML/ MARTE状态机模型到GTS模型的转换方法、从Sys ML/MARTE状态机模型到时间自动机模型的转换方法以及基于UPPAAL工具的系统设计安全性验证过程；第5节在前述模型转换方法的基础上实现了一个基于AMMA的模型转换与验证平台，并给出了实例分析；最后是相关研究工作和总结。
2 Sys ML/MARTE模型
本节主要介绍系统建模语言 Sys ML和MARTE模型，并针对Sys ML中的状态机模型，给出了在本文工作中所构造的结合MARTE语义信息的扩展状态机的元模型，为后面工作提供模型转换与验证的基础。
2.1 Sys ML与MARTE概述
Sys ML是面向系统工程领域并在UML 2.0的基础上进行重用和扩展所得到建模语言，弥补了UML在系统工程领域建模的缺陷，已经成为工业界在系统工程设计与分析过程中的标准建模语言。Sys ML的主要目的是支持在各种复杂系统开发中进行详细规约说明、系统设计、分析与验证等重要过程，因此Sys ML一方面重用了UML中典型的建模元素包，同时使用扩展机制（包括模型元素的定义类型、元类和模型库）对UML中的活动包、类包和辅助包等增加了一些新的语法语义；另一方面还增加了一些 UML没有的新包，如需求包、参数包和分配包［7］。Sys ML建模语言具有的包括硬软件在内系统级信息的特征，使其比较适合应用于现代复杂嵌入式系统领域中的设计与分析研究［7］。
在实时与嵌入式系统领域中进行建模与分析还存在另外一个建模规范MARTE［8］。MARTE是专门针对UML以及Sys ML中尚缺乏对嵌入式系统中所特别关注的各类系统非功能属性进行准确描述的能力而进行的扩展，其包含了相当丰富的系统非功能属性建模元素（如：时间、资源、可靠性、安全性、调度等）。图1中给出了MARTE规范中建模元素包的总体架构。
Figure 1 Package structure of the MARTE图1 MARTE建模元素包的总体结构图
MARTE中建模元素总共分为四个部分：基础包、设计模型包、分析模型包和附件包。其中，基础模型包给出了实时和嵌入式系统中的一些核心概念模型，如优先级、响应时间、执行周期、受限资源等，这些概念是构建系统设计和分析模型的基础。设计模型包中则提供了较高抽象层的建模元素，用于对并发和实时的活动主体和行为进行建模。分析模型包则包含用于对系统的性能和可靠性等进行分析的模型元素。由于 MARTE中具备上述特征，因此我们可以在复杂嵌入式实时系统设计领域中综合采用Sys ML与MARTE的建模能力，并进一步建立相应的分析方法。
2.2 SysML/MARTE的状态机及其元模型构造
状态机（State Machine）是Sys ML中对系统动态行为进行建模的重要模型图之一，它能方便清晰地描述系统动态行为变化。StateMachine包中定义了很多通过有限状态迁移系统对离散行为模型
建模的概念，包括初始状态、终止状态、简单状态、触发事件、卫式、迁移和区域等。图2为一个简单计数功能的Sys ML状态机示例。但是，在典型的Sys ML状态机模型中还缺少资源、时间等方面的非功能属性的完整表达，如：在状态机模型中只是提供了一个简单的时间计时方式等，还不足以用来表达嵌入式实时系统建模分析所需的时间特征。因此，在对复杂嵌入式实时系统建模中，我们还需要结合MARTE中的相关模型元素的语义进行扩展。
在本文工作中首先主要是采用MARTE中有关时间方面的建模元素来对Sys ML中的状态机模型进行扩展，并进一步构建其相应的元模型。由于MARTE自身的扩展机制是基于增加模型元素的注释来实现的，因此，我们可以采用同样的增加状态机模型中的注释的形式来进行扩展并建立元模型。MARTE中的时间建模由时间基、多时间基、时间点和时间结构关系构成。MARTE中的时钟（Clock）是用来访问时间结构的模型元素，可以将状态机中具体的状态、动作、事件或卫式约束关联到时钟实例。MARTE时钟包里面提供了逻辑时间和计时时间，逻辑时间是通过事件发生的次数来定义，计时时间（Chronometric Time）用来描述物理时间；可以处理系统对不同时钟的需求，并能描述系统行为依赖多个时钟以及对系统时间约束的问题［12］，为系统提供计时时间以及对系统时间进行约束。考虑到面向复杂嵌入式实时系统设计中对实时性要求，本文采用了MARTE时间中计时时间的模型语义来扩展状态机。
Figure 2 Sys ML state machine diagram of the counting function图2 计数功能的Sys ML状态机示例
以下给出本文基于SysML规范中状态机中模型元素的定义以及MARTE中时间相关建模元素的分析所构建的Sys ML/MARTE扩展形式的状态机元模型（见图3）。这个元模型图逻辑上可分为两个部分，其一是SysML中的状态机元模型，其中状态机（StateMachine：Sm）由顶点（Vertex）、转换（Transition）和参数（Parameter）三部分组成。区域类（Region）包含状态机所有的状态、状态分组以及状态属性，本文将MARTE中的时钟附加到状态机元模型的Region的属性On中，这样就能在Sys ML状态机任何一个元素上添加时钟约束信息。Exponentialrate、isBranch Point和prob都是和概率相关的元素。Exponentialrate是一个概率表达式，它指明了指数概率分布。isBranch Point用于指明一个状态是否为概率分支。prob指明了迁移可能触发的概率。变迁有一定的约束条件，变迁发生会触发一些动作，还会发生一些行为，状态可以定义不变式，说明状态的约束条件。另一部分是MARTE中的时间相关的元模型，其中Clock代表访问时间，Timed Element是所用计时概念的抽象，将时间元素与非空Clock集联系在一起；Timed Event、Timed Message和TimedProcessing分别表示有时间约束的事件（定期时钟节拍）、消息或活动等；Timed Instant Observation和Timed Duration Obervation则用来表示时钟值或时间间隔，TimedInstantConstraint和TimedDurationConstraint则可以用来表示与时间相关的约束等。
3 AltaRica模型
基于模型的安全性分析（Model-based Safety Analysis）是近年来在实时嵌入式系统工程领域出现的重要研究方向［13］，其基本思想是在系统设计过程中进行系统安全性分析的时候，首先建立包括系统功能行为和故障行为的模型，然后基于模型展开安全性分析与验证，如：构造典型可靠性分析所使用的故障树以及马尔科夫链模型做安全性分析，或者结合形式化验证工具进行验证等。AltaRica［14］就是一种基于形式化的卫式转换（Guarded Transition System）的安全性建模语言，可以用来对复杂安全攸关系统进行建模分析。
AltaRica模型可以分为语法和语义两个层面。
语法层面的表示形式是将系统建模为具备层次结构的节点（Node）集合，每个节点具有多个状态、事件、转换、输入/输出、数据变量等特征，其具体的行为使用类似于自动机的形式来表达。如图4中所给出的AltaRica中一个节点组件的模型示例，它描述了节点具有工作、维修和失效三种状态；当组件处在工作状态时如果发生failure事件，那么组件会转移到失效状态；其他迁移按照同样方式进行。
Figure 4 Example of the AltaRica model图4 AltaRica模型示例
AltaRica在语义层面上是一个卫式转换系统GTS的形式化模型［15］，其严格的定义为一个五元组
虽然AltaRica这种采用状态/转换的高层次模型形式来代替直接设计故障树模型提高了系统工程中设计、共享和维护模型的效率，但是与工业界目前已经认可并使用的Sys ML/MARTE建模语言存在表示形式上较大的不同。因此，本文接下来的主要工作就是建立Sys ML/MARTE行为模型与AltaRica模型之间的语法语义映射关系，设计自动化的模型转换方法，并利用AltaRica模型可以生成故障树的特点，展开基于Sys ML/MARTE模型的系统安全性分析与验证，使得在复杂嵌入式系统设计中只需要熟练掌握Sys ML/MARTE的建模即可，提高系统设计与分析的效率。
Figure 3 Meta-model of the Sys ML/MARTE state machine图3 Sys ML/MARTE扩展形式的状态机元模型
4 系统安全性验证框架
本节中给出基于Sys ML/MARTE模型转换的嵌入式系统设计的安全性验证框架。首先给出了验证框架中总体上模型转换与验证的过程说明，然后分别给出了从SysML/MARTE状态机模型到GTS模型，以及时间自动机模型的转换方法。
4.1 基于模型转换的安全性验证框架
模型驱动工程［17］是近十 年来在 系统 工程 以及软件工程领域中出现的主流方法，其基本思想是以系统模型设计、模型转换与分析/验证为工程开发的重要核心，提高复杂工程系统开发与维护的能力和效率。图5中给出了在MDE架构下本文所设计的基于SysML/MARTE模型转换的嵌入式系统设计安全性质的形式化验证框架。整个框架总体上可以分为三个部分，如下所述：
首先，我们使用扩展形式Sys ML/MARTE状态机模型对嵌入式系统的故障行为进行建模，作为模型转换的源模型；并与此同时构建扩展的状态机元模型与GTS元模型之间的语义映射规则（其中GTS元模型的构造以及语义映射规则在4.2节中详细给出）。这样就可以通过 AMMA平台［11］的模型转换引擎将状态机源模型自动转换成GTS目标模型；然后通过AMMA平台中的TCS［18］组件，在语法层面上将GTS目标模型转换为AltaRica的文本模型。这样就可以使用AltaRica工具来自动构造与系统故障行为相关的故障树模型，并进一步生成系统行为应满足的安全性质（可以用时序逻辑公式来表示）。
当获得了系统行为所需满足的安全性质后，为了能够完成形式化验证，还需要进一步构造系统功能行为的形式化模型。在上述框架中的第二部分中，我们同样可以使用扩展形式的SysML/ MARTE状态机模型对嵌入式系统的功能行为进行建模，作为模型转换的源模型；并通过建立扩展状态机元模型与时间自动机元模型之间的语义映射规则［19］，在 AMMA平台上完成到时间 自动机目标模型的自动转换。之后，为了能够在时间自动机验证工具UPPAAL上展开验证，还通过AMMA平台中的TCS组件将目标模型转换成在UPPAAL工具中所接受的文本格式的模型。
最后，将上述两个层面上转换所得到的表示系统功能行为的时间自动机模型和表示系统安全性质的时序逻辑公式作为验证工具UPPAAL的输入，进行系统行为安全性质的形式化分析验证。
4.2 SysML/MARTE状态机与GTS的元模型转换
为了完成上述的模型转换与验证框架，需要建立Sys ML/MARTE状态机元模型与GTS的元模型之间的语义映射。但是，目前在AltaRica的相关材料中并没有提供GTS相应的元模型，因此在本小节中我们根据AltaRica标准文档中模型元素的说明构建了一个包含其核心建模概念的GTS元模型架构（如图6所示）。
在此架构中，一个GTS模型包含多个节点Node（即系统组件）以及与数据相关的Domains和Constant Values等元素。其中：Domains包含Basic Domain和Compound Domain，基本域是指布尔型、整型、或者范围、枚举等类型，复合域则表示结构、数组等类型；Node模型元素中则包括了Transition、Event、Parameter以及Variable等。Tran-sition中包含卫式（Guard）、事件（Event）和一系列的赋值（Assignment）；Sysc用于定义Node之间的同步，Parameter用于表示在状态前移过程中触发可能事件所需的参数；Variables包含State Value（状态变量）和Flow Value（流变量），其中状态变量的值只有在事件发生时才会改变，流变量是用来表示节点输入/输出接口上数据通信的共享变量。结合2.2节中构造的Sys ML/MARTE状态机的元模型及其语义信息，给出从Sys ML/MARTE状态机元模型到GTS元模型之间的语义映射规则。以下设定S为Sys ML/MARTE状态机的元模型，G为GTS的元模型，二者之间的语义关系Γ即定义了从S到G的映射规则集合，表示为：Γ（S）
Figure 5 Safety verification framework of the Sys ML state machine图5 Sys ML状态机安全性验证框架
G，即函数Γ中包含了一系列的模型元素映射规则，如表1中所示。
映射规则Γ的定义说明包括了基本类型结构、同步以及行为等三个方面。在基本类型结构映射中，Sys ML/MARTE中支持Integer、String、Boolean、DateTime和Real，GTS的基本数据类型有Integer、String、Boolean和Range。根据语义可以直接将Integer、String、Boolean映射为Integer、String、Boolean；而Date Time映射为Integer；Real映射Integer；将Real映射为Range，其中小数点前的数表明范围开始点，小数点后的数表明范围结束。在同步约束映射中，Sys ML/MARTE状态机中的Sync代表状态机中的同步，GTS中的Sync表示各个状态转移的同步性，因此相互映射。在行为映射中，一个Sm映射为一个GTS；Region包含状态 机 中 的 所有 定 义 和 元 素，映 射 到 Node；Sys ML/MARTE状态机中的trigger触发转移，而GTS的Event是触发转移的前提，根据用途因此映射到GTS的Event；状态机的Transition与 GTS的Transition语义是相同的，故而映射；Sys ML/MARTE状态机中的初始状态是Initial-Node直接映射到GTS中的初始状态Init；Sys ML/MARTE状态机中的guard作为转移时必须满足的条件，与GTS上的guard语义相同，直接映射；状态机中的状态（state）表明状态机中的状态，映射到GTS中的statevalue，因为它是作为状态变量，表明系统中各个状态的变化；状态机中的action映射为GTS的flowvalue（表示系统中的数据流动）。
Table 1 Elements of structure mapping between the Sys ML/MARTE state machine and the guard transition system表1 SysML/MARTE状态机与GTS元素映射
Figure 6 Meta-model of the GTS图6 GTS元模型
4.3 Sys ML/MARTE状态机与时间自动机的模型转换
一个时间自动机A的形式化定义是一个四元组
以下给出Sys ML/MARTE状态机元模型与上述时间自动机元模型之间的语义映射规则。不妨设S是Sys ML/MARTE的元模型中的元素集合，T是时间自动机元模型中的元素集合，则二者之间的语义映射关系通过函数∮（ST来表示；即函数∮中包含了一系列的模型元素映射规则，如表2中所示。
映射规则∮的定义说明包括了基本类型结构、时间约束以及行为等三个方面。在基本类型结构映射中，Sys ML/MARTE的基本数据类型有Integer、String、Boolean、DateTime和Real等，而UPPAAL中目前支持Integer、String、Boolean数据类型，根据语义可以直接将Integer、String、Boolean映射；Date Time映射为Integer；Real取小数点前的数值映射为Integer。在时间约束映射中，Timed Instant Observation与Timed Duration Observation分别映射到时间自动机中的时钟，通过观察属性的不同设置成不同的时间约束，Timed Processing表达了事件或者行为的执行时间，并包含了持续期间的属性，使用TimeExpression描述，因此可以直接映到Boolean；Timed Event可以指定事件发生的次数（repetition属性）或者每次发生间隔的时间（every属性），因此直接映到Boolean。状态机中的Region的On代表引入时钟的模型，直接映射到时间自动机中的时钟。在行为映射中，一个Sm映射为一个时间自动机的模板Template；Region包含状态机的所有定义和元素，映射到时间自动机（TA）；状态机中的Vertex同时间自动机的Location都是描述一个状态，所以互相映射；Transition的语义同时间自动机的Transition语义是相同的，故而映射；而状态机中的初始节点Initial Node与自动机中的初始节点Initial映射；要想发生转移则必须满足守卫条件，想要进入状态必须要满足不变式，根据constrant所在位置不同可以分别映射为guard和invariant；Sys ML状态机中的Trigger用来触发转移，TA中的synchronization用于事件的同步性，因此两者相互可以映射；Behavior表示转移时完成的行为与时间自动机的assignment相互映射；Sys ML状态机中的Action表明在状态中需要完成的动作，因此与TA中的Location的赋值相互映射。
Table 2 Elements of structure mapping between the Sys ML/MARTE state machine and the timed automata表2 SysML/MARTE状态机与时间自动机元素映射
5 基于AMMA平台的模型转换与安全性验证方法实现
本小节中首先给出了前述小节所设计的模型转换与安全性验证框架在AMMA平台下的具体实现方法，然后给出了一个简要的示例说明。
5.1 基于AMMA平台的模型转换方法的实现
AMMA是一个在Eclipse环境下支持MDE方法的具有（元）建模、模型转换、模型编织以及模型管理等功能的平台［11］。本文在前面小节的工作基础 上，在 AMMA平台 上设 计并 实现 了 从Sys ML/MARTE状态机模型分别到AltaRica模型以及时间自动机模型的转换，并基于UPPAAL工具展开形式化验证工作。具体而言，AMMA平台中提供了一套模型转换的核心组件：KM3（Kernel Meta Meta Model）、ATL（ATLAS Transform Language）［22，23］、TCS（Textual Concrete Syntax）［18］等。图7是在4.1节中所设计的安全性验证框架中基于AMMA平台的模型转换过程的细化。
Figure 7 Model transformation process of the AMMA platform图7 基于AMMA平台的模型转换过程
基于AMMA平台实现模型之间的语义映射过程实质上是通过ATL语言定义ATL转换规则的过程。我们通过ATL中的命令式指令来声明源模型（Sys ML/MARTE状态机模型）和目标模型（GTS模型）之间的元素关系，然后通过ATL虚拟机的执行将源模型转换为目标模型。在 AMMA平台中我们定义的Sys ML/MARTE状态机元模型与GTS元模型如图8和图9所示，其中包括了构建Sys ML/MARTE活动图元模型与GTS元模型中的每个类，定义每个类中的属性以及类与类之间的关系等。MMs和MMt是Sys ML/ MARTE状态机元模型和GTS元模型。Model-Transform.alt是针对Sys ML/MARTE状态机元模型与GTS元模型在Eclipse的ATL工程下定义的转换文件，通过 ATL虚拟机对转换规则的执行，就可以将Sys ML/MARTE状态机源模型转换成GTS目标模型。表3是在ATL工程中用XMI格式描述的GTS元模型示例。
Figure 8 Meta-model of SysML/MARTE state machine based-on ATL图8 基于ATL的Sys ML/MARTE状态机元模型
Figure 9 Meta-model of the GTS diagram based-on the ATL图9 基于ATL的GTS元模型
Table 3 Description of the Guard_Transition class based-on the XMI表3 基于XMI的Guard_Transition类描述
5.2 实例说明
以下给出了一个飞机着陆控制系统的简单实例说明。飞机着陆控制系统实例的详细说明可参见文献［20，24］，主要包括两组控制对象：飞机（aircraft）和跑道（runway），其中每架飞机具有预计到达时间、最早/最晚到达时间、飞行速度、燃油消耗、是否延误等属性，跑道具有占用时间、进近飞机号、等待飞机号、间隔时间等属性。图10中分别给出了飞机着陆控制系统部分的Sys ML/ MARTE状态机模型（建模工具采用的是Raphsody［25］）。在 状 态 机 模 型 中 主要引 用 了 两 个MARTE建模元素，分别为时钟元素Clock以及资源使用元素Resource Usage，具体名字是时间time和燃油消耗energy，time是飞机到达时间的时钟变量，而energy是飞机消耗的燃油量。
图11表示在5.1节所建立的模型转换框架的主要ATL配置信息过程中，分别设定Sys ML/ MARTE状态机元模型和GTS元模型的文件，并定义输出到目标GTS模型文件中。当我们得到目标GTS模型后，则可以继续通过AltaRica工具［26］（如图12所示）获得系统故障树模型以及表示系统安全性质的时序逻辑公式，所得到安全性质公式示例如下：
Figure 11 ATL configuration图11 ATL配置
（1）E＜＞KL101.done and KL108.done andKL136.done and KL143.done
Figure 12 Interface of the Altarica Studio图12 AltaRica Studio界面
语义描述：着陆系统最终应该将所有空中的飞机都成功地引导落地，不可以出现永远有飞机在空中。
（2）A［］runway0.Idle And In Use imply runway0.Idle AndIn Use
语义描述：处在Idle And In Use的runway0一定还会进入Idle AndInUse状态，即跑道不能永远被占用。
（3）E＜＞KL101.delayed and KL108.on_ time
Figure 10 Aircraft's Sys ML state machine diagram图10 飞机着陆系统的部分状态机模型
描述：表示飞机KL101和飞机KL108可以同时处在delayed状态和approaching状态。
此外，从Sys ML/MARTE建模得到的飞机着陆状态图经过ATL模型转换以及TCS文本转换可以得到相应的时间自动机验证模型，并将转换结果导入到UPPAAL中。图13给出了导入到UPPAAL中的着陆系统的时间自动机模型（在本例中设置飞机的数量为4个，跑道数量为2个）。
飞机着落控制系统的安全性示例验证如下（如图14所示）：
（1）E＜＞KL101.done and KL108.done and KL136.done and KL143.done//验证结果：满足
（2）A［］runway0.Idle AndIn Use imply runway0.Idle AndIn Use//验证结果：满足
（3）E＜＞KL101.delayed and KL108.on_ time//验证结果：满足
6 结束语
与本文相关的研究工作可以分为如下三个方面：第一类工作表明了UML/Sys ML与MARTE的结合使用能够有效地对复杂嵌入式系统的设计进行建模分析，如：文献［24］研究了将UML图（状态机、时序图、活动图）结合 MARTE转换成价格时间自动机并进行验证的方法；文献［27］设计了将UML/MARTE模型向FIACRE形式模型的转换框架，这些转换也是建立在 AMMA平台上利用ATL和TCS来完成；文献［28］研究了基于MDE的实时系统UML模型到形式化模型的模型转换，并进一步进行系统安全性质的形式化证明；文献［19］则给出了Sys ML状态机到时间自动机的转换过程等。第二类工作是与安全性建模与分析语言AltaRica相关的，如：文献［14］中介绍了AltaRica模型，以及在形式化验证中可以发挥的作用；文献［9］研究了如何利用形式化工具来进行AltaRica模型的验证，设计了从AltaRica模型转换到NuSMV的模型转换方法；文献［16］则详细给出了将AltaRica的语义模型GTS转换成故障树的算法；文献［10］给出了AltaRica及其相关工具在航空系统实例中的应用及分析等。第三类相关研究工作是模型驱动工程与形式化方法相结合；如：文献［29］讨论了形式化验证工具可以用在基于模型的开发过程中用来降低降低成本、提高系统开发质量；文献［30］研究了将Sys ML和形式化模型进行
Figure 13 Timed automata model of aitcraft landing in the UPPAAL图13 UPPAAL中飞机着落系统的时间自动机模型
Figure 14 Results of verification图14 验证结果
结合并进行系统安全性分析验证的方法；文献［31］提出了将Sys ML时序图转换成时间自动机并进行形式化验证的方法等。
相比较而言，本文工作是提出了一种基于模型驱动架构的面向Sys ML/MARTE状态机的系统安全性验证方法，具体包括：构建了具备Sys ML/ MARTE扩展语义的状态机元模型，以及安全性建模与分析语言AltaRica的语义模型GTS的元模型；然后建立了从Sys ML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则；并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对Sys ML/ MARTE状态机的模型转换与系统安全性形式化验证的框架，实现了基于模型驱动的嵌入式系统设计安全性验证的一种方法。在接下来进一步的工作中，我们将对具有并发结构的状态机模型的语义转换展开研究，并结合实际工程中某机载航电系统的安全性分析需求展开本文方法的实际应用验证。此外，本文主要研究的是利用现有的一些工具系统，并从技术层面提出了方法和框架进行安全性方法研究，没有从理论层面特别是形式化角度证明模型间语法和语义转换的正确性和完全性问题，这是我接下来进行研究的工作之一。
［1］ Roudier Y，Idrees M S，Apvrille L.Towards the model-driven engineering of safety requirements for embedded systems ［C］∥Proc of IEEE 2013 International Workshop on Model-Driven Requirements Engineering（MoDRE），2013：55-64.
［2］ Hutchinson J，Rouncefield M，Whittle J.Model-driven engineering practices in industry［C］∥Proc of IEEE the 33rd International Conference on Software Engineering（ICSE），2011：633-642.
［3］ Hästbacka D，Vepsäläinen T，Kuikka S.Model-driven development of industrial process control applications［J］.Journal of Systems and Software，2011，84（7）：1100-1113.
［4］ Moy Y，Ledinot E，Delseny H，et al.Testing or formal verification：DO-178C alternatives and industrial experience［J］. IEEE Software，2013，30（3）：50-57.
［5］ Reif W.Model based safety analysis［C］∥Proc of Dependable Control of Discrete Systems，2009：3.
［6］ Biehl M，Dejiu C，Törngren M.Integrating safety analysis into the model-based development toolchain of automotive embedded systems［C］∥Proc of ACM Sigplan Notices，2010：125-132.
［7］ Friedenthal S，Moore A，Steiner R.A practical guide to SysML：The systems modeling language［M］.New York： Elsevier，2011.
［8］ Selic B，Gérard S.Modeling and analysis of real-time and embedded systems with UML and MARTE：Developing cyber-physical systems［M］.New York：Elsevier，2013.
［9］ Bozzano M，Cimatti A，Lisagor O，et al.Symbolic model checking and safety assessment of altarica models［J］.Electronic Communications of the EASST，2011，46（2011）：1.
［10］ Bieber P，Bougnol C，Castel C，et al.Safety assessment with AltaRica-lessons learnt based on two aircraft system studies［C］∥Proc of the 18th IFIP World Computer Congress，Topical Day on New Methods for Avionics Certification.Citeseer，2004：1.
［11］ Atlan Mod Team，INRIA.AMMA home［EB/OL］.［2008-01-07］.http：//wiki.eclipse.org/index.php/AMMA.
［12］ Rioux L，Saunier T，Gérard S，et al.MARTE：A new profile RFP for the modeling and analysis of real-time embedded systems［C］∥Proc of UML-SoC'05，2005：1.
［13］ Güdemann M.Qualitative and quantitative formal modelbased safety analysis［D］.Magdeburg：Ottovon Guericke U-niversity，2011.
［14］ Prosvirnova T，Batteux M，Brameret P，et al.The altarica 3.0 project for model-based safety assessment［C］∥Proc of IEEE the 4th IFAC Workshop on Dependable Control of Discrete Systems（DCDS），2013：1.
［15］ Rauzy A B.Guarded transition systems：A new states/events formalism for reliability studies［J］.Proceedings of the Institution of Mechanical Engineers，Part O：Journal of Risk and Reliability，2008，222（4）：495-505.
［16］ Prosvirnova T，Rauzy A.AltaRica 3.0 project：Compile guarded transition systems into fault trees［J］.Proceedings of ESREL2013，2013，20（3）：485-491.
［17］ Rutle A，Rossini A，Lamo Y，et al.A formal approach to the specification and transformation of constraints in MDE ［J］.The Journal of Logic and Algebraic Programming，2012，81（4）：422-457.
［18］ Ruscio D D，Iovino L，Pierantonio A.Managing the coupled evolution of metamodels and textual concrete Syntax specifications［C］∥Proc of IEEE the 39th EUROMICRO Conference on Software Engineering and Advanced Applications（SEAA），2013：114-121.
［19］ Huang Xiao-pu.Research on MDE based model transformation［D］.Nanjing：Nanjing University，2013.（in Chinese）
［20］ Behrmann G，David A，Larsen K G，et al.UPPAAL 4.0 ［C］∥Proc of IEEE the 3 rd International Conference on Quantitative Evaluation of Systems（QEST 2006），2006：125-126.
［21］ UPPAAL tutorial［EB/OL］.［2013-01-09］.http：//w ww. it.uu.se/research/group/darts/uppaal/flat-1_1.dtd.
［22］ Jouault F，Tisi M.Towards incremental execution of ATL transformations［M］∥Theory and Practice of Model Transformations，Berlin：Springer，2010：123-137.
［23］ ATLAS group，LINA&INRIA Nantes.ATL：Atlas trans-for-Mationlanguage［EB/OL］.［2006-01-01］.http//www.eclipse.org/m2m/atl/doc/ATL_User_Manual%5Bv07%5D. pdf，2006.
［24］ Ji Ming.The method research on resource modeling and verification of real-time software based on model transformation［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2010.（in Chinese）
［25］ Harel D，Kugler H.The rhapsody semantics of statecharts （or，on the executable core of the U ML）［M］∥Integration of Software Specification Techniques for Applications in Engineering，Berlin：Springer，2004：325-354.
［26］ Rauzy A.AltaRica Down Load［EB/OL］.［2014-12-07］.http//www.eclipse.org/m2m/atl/http：//altarica.labri.fr/ pub/tools/packages/current/arc-current.tar.gz.
［27］ Zhang Tian，Jouault F，Attiogbe C.MDE-Based model to FIACRE model［J］.Journal of Software，2009，20（2）：214-233.（in Chinese）
［28］ Liu Ya-ping，Research on model transformation method of real-time system based on metamodeling［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2010.（in Chinese）
［29］ Whalen M，Cofer D，Miller S，et al.Integration of formal analysis into a model-based software development process ［M］∥Formal Methods for Industrial Critical Systems，Berlin：Springer，2008：68-84.
［30］ Pétin J，Evrot D，Morel G，et al.Combining Sys ML and formal methods for safety requirements verification［C］∥Proc of the 22nd International Conference on Software& Systems Engineering and their Applications，2010：115-122.
［31］ Cui Kang-le.Research on UML timing diagram model to UPPAAL timed automata model transformation method and its tool to achieve［D］.Shanghai：East China Normal University，2011.（in Chinese）
附中文参考文献：
［19］ 黄小浦.基于 MDE模型转换的若干研究［D］.南京：南京大学，2013.
［24］ 吉鸣.基于模型转换的实时软件资源建模与验证的方法研究［D］.南京：南京航空航天大学，2010.
［27］ 张天，Jouault F，Attiogbe C，等.基于MDE的异构模型转换从MARTE模型到FIACRE模型［J］.软件学报，2009，20 （2）：214-233.
［28］ 刘亚萍.基于MDE的UML模型到形式化模型的转换方法研究［D］.南京：南京航空航天大学，2009.
［31］ 崔康乐.UML时序图模型到UPPAAL时间自动机模型转换方法研究和工具实现［D］.上海：华东师范大学，2011.
刘雪（1989），女，安徽宿州人，硕士生，研究方向为软件工程和软件建模与分析。E-mail：lx_029@nuaa.edu.cn
LIU Xue，born in 1989，MS candidate，her research interests include software engineering，and software modeling and analysis.
胡军（1973），男，湖北黄冈人，博士，副教授，研究方向为模型驱动的系统安全性分析、软件验证和嵌入式系统设计。E-mail：hujun.nju@139.com
HU Jun，born in 1973，PhD，associate professor，his research interests include model-based safety analysis，software analysis，and formal methods.
黄志球（1965 ），男，江苏南京人，博士后，博士生导师，研究方向为软件工程和软件度量。E-mail：zqhuang@nuaa.edu.cn
HUANG Zhi-qiu，born in 1965，post doctor，PhD supervisor，his research interests include software engineering，and software metrics.
马金晶（1990 ），男，安徽合肥人，硕士生，研究方向为软件分析和模型检测。E-mail：majinjing3@vip.qq.com
MA Jin-Jing，born in 1990，MS candidate，his research interests include software analysis，and model checking.
程桢（1990 ），男，安徽安庆人，硕士生，研究方向为软件分析和模型检测。E-mail：604246353@qq.com
CHENG Zhen，born in 1990，MS candidate，his research interests include software analysis，and model checking.
石娇洁（1990 ），女，河南郑州人，硕士生，研究方向为软件分析和模型检测。E-mail：shijiaojiexzs@163.com
SHI Jiao-jie，born in 1990，MS candidate，her research interests include software analysis，and model checking.
Research on model driven safety verification for embedded system designs
LIU Xue1，HU Jun1，2，HUANG Zhi-qiu1，MA Jin-jing1，CHENG Zhen1，SHI Jiao-jie1
（1.School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing 210016；
2.State Key Laboratory for Novel Software Technology，Nanjing University，Nanjing 210093，China）
In recent years the model based safety analysis and verification method for embedded systems is an important research hotspot in the field of safety critical systems engineering.We put forward a system safety verification method based on the model driven architecture，which is Sys ML/MARTE state machine oriented，including the construction of both the state machine metamodel which has Sys ML/MARTE extension semantics，and the GTS metamodel which is the semantic model of AltaRica （ie.safety modeling and analysis language）.We then establish semantic mapping model transformation rules from a Sys ML/MARTE state machine model to the timed automata model and to the AltaRica model respectively.Thirdly，based on the platform of the AMMA and the timed automata verification tools UPPAAL we design and realize the model transformation of the Sys ML/MARTE state machine and the framework for system safety formal verification.Finally a safety verification example about aircraft landing control system design model is analyzed.
system safety analysis；model-driven engineering；Sys ML/MARTE；state machine model；embedded system
TP311.5
A
10.3969/j.issn.1007-130X.2015.08.013
1007-130X（2015）08-1498-12
2014-09-01；
2014-11-25
国家重点基础研究发展计划973计划资助项目（2014CB744904）；国家自然科学基金资助项目（61100034，61170043）；南
京航空航天大学青年科技创新基金资助项目（NS2014098）；回国留学人员科研启动基金资助项目（2012）
通信地址：210016江苏省南京市南京航空航天大学计算机科学与技术学院
Address：School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing 210016，Jiangsu，
P.R.China
