模型驱动的嵌入式系统设计安全性验证方法研究

作     者：刘雪 胡军 黄志球 马金晶 程桢 石娇洁 LIU Xue;HU Jun;HUANG Zhi-qiu;MA Jin-jing;CHENG Zhen;SHI Jiao-jie

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

基　　金：国家重点基础研究发展计划973计划资助项目(2014CB744904) 国家自然科学基金资助项目(61100034 61170043) 南京航空航天大学青年科技创新基金资助项目(NS2014098) 回国留学人员科研启动基金资助项目(2012) 

出 版 物：《计算机工程与科学》 (Computer Engineering & Science)

年 卷 期：2015年第37卷第8期

页      码：1498-1509页

摘      要：基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。

主 题 词：系统安全性分析 模型驱动工程 SysML/MARTE 状态机模型 嵌入式系统 

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

核心收录：

D　O　I：10.3969/j.issn.1007-130X.2015.08.013

馆 藏 号：203233284...