本发明公开了一种基于S~2ML的安全攸关系统分析与验证方法,其特点是采用Z3约束求解器对生成的数据文件进行性质验证的方法,具体包括:读取格式文件、抽取每个状态之间迁移的条件、转换成约束求解的格式和性质分析等步骤。本发明与现有技术相比具有较高的求解效率,极大的提高系统的可靠性与安全性,较好的解决了SysML的状态机图不支持自动检测系统的安全性的问题,方法简便,成本低廉且安全可靠。