从STPA到安全行为模型
From STPA to Safe Behavior Models
AI总结：
本文提出从STPA风险分析结果自动生成LTL公式并综合出安全行为模型的方法，同时扩展STPA以覆盖活性性质，为安全关键系统建模提供基础。
摘要：
模型检验是一种经过验证的方法，用于检查安全关键系统的行为模型是否满足以LTL公式表述的安全性质。我们提出基于风险分析技术系统理论过程分析（STPA）的结果自动生成此类LTL公式的规则。此外，我们提出从这些生成的LTL公式综合出安全行为模型。为了在模型中同时覆盖活性性质，我们用期望控制动作扩展STPA。我们使用SCCharts作为行为模型在一个示例系统上演示了该方法。所得模型不一定是完整的，但提供了一个良好的基础，已经覆盖了安全性和活性性质。
英文摘要：
Model checking is a proven approach for checking whether the behavior model of a safety-critical system fulfills safety properties that are stated as LTL formulas.We propose rules for generating such LTL formulas automatically based on the result of the risk analysis technique System-Theoretic Process Analysis (STPA). Additionally, we propose a synthesis of a Safe Behavior Model from these generated LTL formulas. To also cover liveness properties in the model, we extend STPA with Desired Control Actions. We demonstrate our approach on an example system using SCCharts for the behavior model. The resulting model is not necessarily complete but provides a good foundation that already covers safety and liveness properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
