From STPA to Safe Behavior Models

模型检查是一种已被证明的方法，用于检查安全关键系统的行为模型是否满足以LTL公式陈述的安全属性。我们提出了一些规则，根据风险分析技术System-Theoretic Process Analysis（STPA）的结果自动生成这些LTL公式。此外，我们提出了从这些生成的LTL公式中合成安全行为模型的方法。为了在模型中也涵盖活性属性，我们使用期望控制操作扩展了STPA。我们使用SCCharts作为行为模型，在一个示例系统上演示了我们的方法。生成的模型不一定完整，但提供了一个良好的基础，已经涵盖了安全和活性属性。

论文提出一种基于STPA和LTL公式的自动生成安全性行为模型的方法，以解决安全关键系统的安全性问题。

通过STPA进行风险分析，自动生成LTL公式，并从中合成出安全性行为模型，以覆盖系统的安全性和活性属性。

论文在SCCharts上演示了该方法，并提出了扩展STPA以覆盖活性属性的Desired Control Actions。

在此领域的相关研究包括模型检查、STPA等方法的应用，以及基于LTL公式的自动生成安全性行为模型的研究。