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

来源：计算机工程与科学杂志2015年第8期北京时间：

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

单位：1.南京航空航天大学计算机科学与技术学院，江苏 南京 210016;2.南京大学计算机软件新技术国家重点实验室，江苏 南京 210093

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

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

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