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

作     者：黄传林 黄志球 胡军 徐丙凤 曲长亮 HUANG Chuan-lin;HUANG Zhi-qiu;HU Jun;XU Bing-feng;QU Chang-liang

作者机构：南京航空航天大学计算机科学与技术学院南京210016 南京大学计算机软件新技术国家重点实验室南京210093 

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

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2015年第36卷第3期

页      码：408-417页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203320412...