近年来，随着航空、交通、医疗等安全关键系统的规模越来越大，涉及到的复杂度也越来越高，基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向，因而如何对以 SysML为典型的系统模型进行安全性分析与验证是一个非常重要的问题。文中以基于模型的安全性分析（MBSA）为框架，设计了一个面向SysML模型的系统安全性分析与验证方法，实现了从模型构建至安全性分析与属性验证的完整过程。首先，从需求层面和设计层面对SysML系统架构设计模型和最新系统安全性建模语言AltaRica3.0进行了介绍，构建了从SysML的核心模型元素到AltaRica3.0模型的语义等价的转换规则，给出了转换规则的形式化描述并分析证明转换规则的正确性；然后，基于模型驱动的方法设计了一个原型工具平台来完成模型的自动转换和安全性分析过程，该原型工具集成了转换、编译生成故障树、故障树分析、单步仿真及故障路径动态演示功能，实现了系统设计和安全性分析的同步性，并在其基础上给出了AltaRica3.0至Promela模型的转换关键点，结合穷尽式模型验证工具SPIN对模型的属性进行安全性验证；最后，根据4761标准中对机轮刹车系统的体系结构设计描述和安全性的需求建立SysML模型，依据原型工具平台和属性验证工具实现模型的自动转换和安全性分析验证，进而来说明此转换方法的有效性。