一种基于S～2ML的安全攸关系统分析与验证方法

作者：刘静; 杨琛琛; 孙海英; 康介祥; 尹伟; 高忠杰; 王辉; 吴志伟; 丁郭欢

来源：2020-12-22, 中国, ZL202011524084.0.

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