一种基于STPA的软件安全性分析与验证方法

安全性苛求系统的安全性关系关系着人们生命财产安全,而软件与系统的安全性紧密相关。形式化验证方法可以证明软件的正确性,但并不能保证软件的安全性性。系统理论危害分析方法(System-Theoretic Process Analysis,STPA)是一种基于系统理论的危害分析方法,它可以识别系统中的危害并得到软件相关的安全性需求。本文提出一个结合STPA与模型检测的软件安全性分析与验证方法:使用STPA对系统进行危害分析得到软件安全性需求,形式化描述软件安全性性质,最后使用模型检测的方法验证软件安全性。