计算机应用

作者：秦楠, 马亮, 黄锐

单位：海军潜艇学院, 山东 青岛 266199

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

基金：国家自然科学基金资助项目（51377169）。

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

来源：2020年第11期

《计算机应用》期刊编辑部

查看计算机应用杂志2020年第11期