基于系统理论过程分析的软件安全性需求分析与验证方法

Software safety requirement analysis and verification method based on system theoretic process analysis

针对传统系统理论过程分析(STPA)方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。

There are two problems to be solved in the traditional System Theoretic Process Analysis(STPA)method.One is the lack of automation means of realization,the other is the ambiguity problem caused by natural language result analysis.To solve these problems,a software safety requirement analysis and verification method based on STPA was proposed.Firstly,the software safety requirements were extracted and converted into formal expressions by the algorithm.Secondly,the state diagram model was built to describe the logic of software safety control behaviors and converted the logic into the readable formal language.Finally,the formal verification was carried out by model checking technology.The effectiveness of the method was verified by the case of a weapon launch control system.The results show that the proposed method can generate the safety requirements automatically and perform formal verification to them,avoid the dependence on manual intervention and solve the natural language description problems in traditional methods.