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

摘要：

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

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

所属期刊栏目：37

分类号：TP311.5(计算技术、计算机技术)

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

在线出版日期：2015-09-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1498-1509