[1]石娇洁[],胡军[],刘雪[],等. 一种嵌入式系统模型的安全性分析验证方法[J].计算机技术与发展,2015,25(10):7-12.
　SHI Jiao-jie[],HU Jun[],LIU Xue[],et al. A Verification Method of Security Analysis for Embedded System Model[J].,2015,25(10):7-12.
点击复制

 一种嵌入式系统模型的安全性分析验证方法()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
25
期数:
2015年10期
页码:
7-12
栏目:
智能、算法、系统工程
出版日期:
2015-10-10

文章信息/Info

Title:
 A Verification Method of Security Analysis for Embedded System Model
文章编号:
1673-629X（2015)10-0007-06
作者:
 石娇洁[1]; 胡军[2]; 刘雪[1]; 马金晶[1]; 黄志球[1]; 程桢[1]
 1.南京航空航天大学 计算机科学与技术学院；2. 南京大学 计算机软件新技术国家重点实验室
Author(s):
 SHI Jiao-jie[1]; HU Jun[2]; LIU Xue[1]; MA Jin-jing[1]; HUANG Zhi-qiu[1]; CHENG Zhen[1]
关键词:
 ; 系统安全性分析; 模型驱动; SysML/MARTE ; XFTA ; 状态机模型; 嵌入式系统模型
Keywords:
 ; system safety analysis; model driven; SysML/MARTE; XFTA; state machine model; embedded system model
分类号:
TP31
文献标志码:
A
摘要:
 由于嵌入式系统模型设计周期越来越短，功能越来越复杂，其安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。针对这种情况，文中提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性分析验证方法。具体包括：构建了具备SysML/MARTE扩展语义的状态机元模型，以及高级安全性建模与分析语言AltaRica的语义模型GTS的元模型，然后建立了从SysML/MARTE状态机模型到AltaRica模型的语义映射模型转换规则，并基于AMMA平台和故障树分析工具XFTA实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证框架的构建。最后给出了民用飞机系统中的机轮刹车系统设计模型的例子进行实例验证分析。实验结果表明，提出的嵌入式系统设计模型的安全性分析与验证方法是具有代表性和可执行性的。
Abstract:
 Because the design cycle of embedded system model is shorter and shorter,the function is more and more complex,in the field of safety critical systems engineering,its security analysis and verification method is an important research hotspot in recent years. In view of this,put forward a method based on model driven architecture for system security analysis verification, which is oriented SysML/MARTE state machine,including that constructed the state machine metamodel which has SysML/MARTE extension semantics,and the GTS metamodel which is the semantic model of AltaRica,high safety modeling and analysis language,then established semantic mapping model transformation rules from the SysML/MARTE state machine model to the AltaRica model,and based on the platform of AMMA and the fault tree analysis tools XFTA to realize the model transformation of SysML/MARTE state machine and the framework for system security formal verification. Finally give security verification example about wheel brake system design model. Experimental results show that the proposed verification method of security analysis for embedded system design model is representative and executive.

相似文献/References:

[1]张志宏,吴庆波,邵立松,等.基于飞腾平台TOE协议栈的设计与实现[J].计算机技术与发展,2014,24(07):1.
　ZHANG Zhi-hong,WU Qing-bo,SHAO Li-song,et al. Design and Implementation of TCP/IP Offload Engine Protocol Stack Based on FT Platform[J].,2014,24(10):1.
[2]梁文快,李毅. 改进的基因表达算法对航班优化排序问题研究[J].计算机技术与发展,2014,24(07):5.
　LIANG Wen-kuai,LI Yi. Research on Optimization of Flight Scheduling Problem Based on Improved Gene Expression Algorithm[J].,2014,24(10):5.
[3]黄静,王枫,谢志新,等. EAST文档管理系统的设计与实现[J].计算机技术与发展,2014,24(07):13.
　HUANG Jing,WANG Feng,XIE Zhi-xin,et al. Design and Implementation of EAST Document Management System[J].,2014,24(10):13.
[4]侯善江[],张代远[][][]. 基于样条权函数神经网络P2P流量识别方法[J].计算机技术与发展,2014,24(07):21.
　HOU Shan-jiang[],ZHANG Dai-yuan[][][]. P2P Traffic Identification Based on Spline Weight Function Neural Network[J].,2014,24(10):21.
[5]李璨,耿国华,李康,等. 一种基于三维模型的文物碎片线图生成方法[J].计算机技术与发展,2014,24(07):25.
　LI Can,GENG Guo-hua,LI Kang,et al. A Method of Obtaining Cultural Debris’ s Line Chart Based on Three-dimensional Model[J].,2014,24(10):25.
[6]翁鹤,皮德常. 混沌RBF神经网络异常检测算法[J].计算机技术与发展,2014,24(07):29.
　WENG He,PI De-chang. Chaotic RBF Neural Network Anomaly Detection Algorithm[J].,2014,24(10):29.
[7]刘茜[],荆晓远[],李文倩[],等. 基于流形学习的正交稀疏保留投影[J].计算机技术与发展,2014,24(07):34.
　LIU Qian[],JING Xiao-yuan[,LI Wen-qian[],et al. Orthogonal Sparsity Preserving Projections Based on Manifold Learning[J].,2014,24(10):34.
[8]尚福华,李想,巩淼. 基于模糊框架-产生式知识表示及推理研究[J].计算机技术与发展,2014,24(07):38.
　SHANG Fu-hua,LI Xiang,GONG Miao. Research on Knowledge Representation and Inference Based on Fuzzy Framework-production[J].,2014,24(10):38.
[9]叶偲,李良福,肖樟树. 一种去除运动目标重影的图像镶嵌方法研究[J].计算机技术与发展,2014,24(07):43.
　YE Si,LI Liang-fu,XIAO Zhang-shu. Research of an Image Mosaic Method for Removing Ghost of Moving Targets[J].,2014,24(10):43.
[10]余松平[][],蔡志平[],吴建进[],等. GSM-R信令监测选择录音系统设计与实现[J].计算机技术与发展,2014,24(07):47.
　YU Song-ping[][],CAI Zhi-ping[] WU Jian-jin[],GU Feng-zhi[]. Design and Implementation of an Optional Voice Recording System Based on GSM-R Signaling Monitoring[J].,2014,24(10):47.

更新日期/Last Update: 2015-11-09