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

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

作　　者：秦楠[1] 马亮[1] 黄锐[1] QIN Nan;MA Liang;HUANG Rui(Naval Submarine Academy,Qingdao Shandong 266199,China)

机构地区：[1]海军潜艇学院,山东青岛266199

出　　处：《计算机应用》2020年第11期3261-3266,共6页journal of Computer Applications

基　　金：国家自然科学基金资助项目(51377169)。

摘　　要：针对传统系统理论过程分析(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.

关 键 词：系统理论过程分析 软件安全需求 形式化方法 模型检验 武器发射控制系统 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论] TJ63[自动化与计算机技术—计算机科学与技术]