面向AltaRica模型的系统安全性设计验证方法

摘要

本发明公开了一种步骤一：建立系统安全性设计AltaRica模型；步骤二：定义AltaRica模型到Promela模型间模型转换的规则；得到AltaRica模型转换之后的Promela模型；步骤三：使用线性时序逻辑对系统安全需求需求进行形式化的描述；步骤四：利用模型检测器对系统模型进行安全性验证；步骤五：得到不满足步骤四的安全性需求反例，对系统安全性设计模型进行追踪，完成系统安全性设计模型的验证。本发明有效地解决模型转换问题，完成了模型检测工具SPIN对AltaRica的操作。本发明是一种针对系统安全性分析的新思路，使得转换规则定义的更精确。

主权项

面向AltaRica模型的系统安全性设计验证方法，其特征在于，包括如下步骤：步骤一：建立系统安全性设计AltaRica模型；步骤二：得到AltaRica模型转换之后的Promela模型；步骤三：使用线性时序逻辑对系统安全需求需求进行形式化的描述；步骤四：以步骤二的转换后的Promela模型、步骤三使用线性时序逻辑规约的安全性需求作为输入，利用模型检测器对系统模型进行安全性验证；步骤五：对步骤四模型检测工具的验证结果进行分析，并得到不满足步骤四的安全性需求反例，对系统安全性设计模型进行追踪，完成系统安全性设计模型的验证。