中文摘要：

能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括：构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析.

英文摘要：

In the areas of energy, transportation and others, the safety verification and analysis of complex embedded system design has become one of the important research;this paper presents an extended SysML activity diagram model combined with MARTE semantic information, which used to describe the design of dynamic embedded system behavior in safety-critical applications, and has a research of the formal safety analysis and verification for the system design having safety features based on model transformation, which is as follow： constructs the meta-model of SysML activity diagram combined with non-functional modeling semantic of MARTE and timed automata used in the UPPAAL one of model checker tools, then, gives the semantic mapping rules between the two ; constructs the syn- tax transformation between the description of timed automata model and the input format of UPPAAL;designs the model transforma- tion and verification framework for the extended SysML activity diagram based on the AMMA platform;finally,has a safety verifica- tion of a design model of control system in high-speed rail.