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

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