Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From STPA to Safe Behavior Models

Jette Petzold, Reinhard von Hanxleden

TL;DR

The paper addresses safe verification of safety-critical systems by automatically deriving LTL safety properties from STPA results and synthesizing a Safe Behavior Model (SBM) in SCCharts. It introduces new translation rules for multiple unsafe-control-action types, extends STPA with Desired Control Actions to cover liveness, and provides an end-to-end pipeline implemented in the pasta tool with an ACC example. The key contributions are the expanded STPA-to-LTL translation, automatic SBM generation, and the DCA extension, which together produce a safety-and-liveness compliant behavior model, albeit with incompleteness in initialization and variable calculations that require developer augmentation. This approach tightens the integration between risk analysis and model-based design, reducing manual formula generation and enabling safer automatic code synthesis from safety analysis results.

Abstract

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.

From STPA to Safe Behavior Models

TL;DR

The paper addresses safe verification of safety-critical systems by automatically deriving LTL safety properties from STPA results and synthesizing a Safe Behavior Model (SBM) in SCCharts. It introduces new translation rules for multiple unsafe-control-action types, extends STPA with Desired Control Actions to cover liveness, and provides an end-to-end pipeline implemented in the pasta tool with an ACC example. The key contributions are the expanded STPA-to-LTL translation, automatic SBM generation, and the DCA extension, which together produce a safety-and-liveness compliant behavior model, albeit with incompleteness in initialization and variable calculations that require developer augmentation. This approach tightens the integration between risk analysis and model-based design, reducing manual formula generation and enabling safer automatic code synthesis from safety analysis results.

Abstract

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.
Paper Structure (28 sections, 1 theorem, 12 equations, 7 figures)

This paper contains 28 sections, 1 theorem, 12 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Contributions & Outline
  3. Background
  4. stpa
  5. Statecharts
  6. ltl
  7. Related Work
  8. stpa to ltl
  9. Formula for Not-Provided
  10. Formula for Too-Late
  11. Formula for Too-Early
  12. Formula for Applied-Too-Long
  13. Formula for Stopped-Too-Soon
  14. stpa to sbm
  15. States
  16. ...and 13 more sections

Key Result

theorem thmcountertheorem

For an sbm created with the proposed construction rules, no trace exists that violates one of the ltl formulas, except possibly the ones for the type too-early.

Figures (7)

  • Figure 1: Traces for the different uca types that are prevented by the proposed formulas. Here, we do not consider the first reaction of a trace.
  • Figure 2: Translation of uca types provided and not-provided to statecharts. $A$ is the statechart without the state $s_{ca}$.
  • Figure 3: Translation of uca type applied-too-long. $A$ is the statechart without the state $s_{ca}$.
  • Figure 4: Translation of uca type stopped-too-soon. $A$ is the statechart without the state $s_{ca}$.
  • Figure 5: Automatically generated sbm for the acc example.
  • ...and 2 more figures

Theorems & Definitions (2)

  • theorem thmcountertheorem
  • proof