  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.
