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

摘要：

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

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

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2016-09-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：408-417