一种基于STPA的安全关键软件安全性验证方法

摘要

一种基于STPA的安全关键软件安全性验证方法。其包括对安全关键软件进行STPA分析及形式化规约，得到软件安全约束；采用形式化建模符号将步骤1中得到的软件安全约束转换为模型检测过程所需的安全规约模型，然后，在安全规约模型检测工具中将基于功能需求建立的软件设计模型与安全规约模型中相应的变量进行连接，由此完成对安全关键软件安全性的形式化验证等步骤。本发明效果：解决了传统分析方法很难捕获组件交互和复杂条件下的软件危险行为，以及安全性验证依赖人工的问题。