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

Research on model driven safety verification for embedded system designs

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

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

出　　处：《计算机工程与科学》2015年第8期1498-1509,共12页Computer Engineering & Science

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

摘　　要：基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。In recent years the model based safety analysis and verification method for embedded systems is an important research hotspot in the field of safety critical systems engineering. We put forward a system safety verification method based on the model driven architecture, which is SysML/MARTE state machine oriented, including the construction of both the state machine metarnodel which has SysML/MARTE extension semantics, and the GTS metamodel which is the semantic model of AltaRiea （ie. safety modeling and analysis language）. We then establish semantic mapping model transformation rules from a SysML/MARTE state machine model to the timed automata model and to the AltaRica model respectively. Thirdly, based on the platform of the AMMA and the timed automata verification tools UPPAAL we design and realize the model transformation of the SysML/MARTE state machine and the framework for system safety formal verification. Finally a safety verification example about aircraft landing control system design model is analyzed.

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

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