基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究  

Research on Safety Verification of Extended SysML Activity Diagram for Embedded System Design

作　　者：黄传林 黄志球[1] 胡军[1,2] 徐丙凤[1] 曲长亮[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《小型微型计算机系统》2015年第3期408-417,共10页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61100034;61170043)资助;中国博士后科学基金项目(20110491411)资助;江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助

摘　　要：能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合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.

关 键 词：嵌入式系统安全性分析 SysML活动图 MARTE 模型转换 形式化方法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]