一种软件控制危险分析方法

摘要

本发明提供一种软件控制危险分析方法，包括：基于目标有限状态软件系统状态机模型转换而成的C语言程序状态机模型，生成中间语言状态机模型，所述中间语言状态机模型通过中间变量的初始值、转移条件、转移前取值和转移后取值表征；基于所述中间语言状态机模型，获取中间语言状态机转移和所述中间变量的取值集合；基于所述中间变量的变量类型、取值集合、初始值和所述中间语言状态机转移，获取SMV程序状态机模型；基于所述SMV程序状态机模型，在NuSMV模型检测工具中执行状态机模型检测程序，输出检测结果。本发明能够实现目标有限状态软件系统状态机模型的准确且有效检测，从而使得对软件安全性分析的过程和结果更为简洁、直观。