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

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

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