Journal of Computer Applications ›› 2020, Vol. 40 ›› Issue (11): 3261-3266.DOI: 10.11772/j.issn.1001-9081.2020040548

• Computer software technology • Previous Articles     Next Articles

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

QIN Nan, MA Liang, HUANG Rui   

  1. Naval Submarine Academy, Qingdao Shandong 266199, China
  • Received:2020-04-27 Revised:2020-07-02 Online:2020-11-10 Published:2020-07-20
  • Supported by:
    This work is partially supported by the National Natural Science Foundation of China (51377169).


秦楠, 马亮, 黄锐   

  1. 海军潜艇学院, 山东 青岛 266199
  • 通讯作者: 秦楠(1988-),女,山东青岛人,工程师,博士研究生,主要研究方向:系统安全性分析、形式化验证;
  • 作者简介:马亮(1973-),女,吉林镇赉人,教授,博士,主要研究方向:船舶航行安全、系统安全性分析;黄锐(1981-),男,山东莱阳人,讲师,硕士,主要研究方向:系统安全性分析
  • 基金资助:

Abstract: 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.

Key words: System Theoretic Process Analysis (STPA), software safety requirement, formal method, model checking, weapon launch control system

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

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

CLC Number: