From STPA to Safe Behavior Models
arxiv(2024)
摘要
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 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要