一种嵌入式系统模型的安全性分析验证方法  

A Verification Method of Security Analysis for Embedded System Model

作　　者：石娇洁 胡军[1,2] 刘雪[1] 马金晶[1] 黄志球[1] 程桢[1] 

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

出　　处：《计算机技术与发展》2015年第10期7-12,共6页Computer Technology and Development

基　　金：国家"973"重点基础研究发展计划项目(2014CB744903);回国留学人员科研启动基金(2012);611航空科研基金(2012);南京航空航天大学青年科技创新基金(NS2014098)

摘　　要：由于嵌入式系统模型设计周期越来越短,功能越来越复杂,其安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。针对这种情况,文中提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性分析验证方法。具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及高级安全性建模与分析语言AltaRica的语义模型GTS的元模型,然后建立了从SysML/MARTE状态机模型到AltaRica模型的语义映射模型转换规则,并基于AMMA平台和故障树分析工具XFTA实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证框架的构建。最后给出了民用飞机系统中的机轮刹车系统设计模型的例子进行实例验证分析。实验结果表明,提出的嵌入式系统设计模型的安全性分析与验证方法是具有代表性和可执行性的。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 roles 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.

关 键 词：系统安全性分析 模型驱动 SysML/MARTE XFTA 状态机模型 嵌入式系统模型 

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