From STPA to Safe Behavior Models

• URL: http://arxiv.org/abs/2404.04093v1
• Date: Fri, 5 Apr 2024 13:39:25 GMT
• Title: From STPA to Safe Behavior Models
• Authors: Jette Petzold, Reinhard von Hanxleden,
• Abstract summary: We propose rules for generating safetycritical formulas based on the result-critical System-Theoretic Process Analysis (STPA) To also cover liveness properties in a behavior model, we extend A with Desired Control Actions. The resulting model is not necessarily complete but provides a good foundation that already covers safety and liveness properties.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Semi-supervised Regression Analysis with Model Misspecification and High-dimensional Data [8.619243141968886]
  We present an inference framework for estimating regression coefficients in conditional mean models. We develop an augmented inverse probability weighted (AIPW) method, employing regularized estimators for both propensity score (PS) and outcome regression (OR) models. Our theoretical findings are verified through extensive simulation studies and a real-world data application.
  arXiv  Detail & Related papers  (2024-06-20T00:34:54Z)
• Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions [44.99833362998488]
  We develop an abstraction framework that can be used to solve this problem under various modeling assumptions. We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model.
  arXiv  Detail & Related papers  (2023-11-16T11:03:54Z)
• Neural Abstractions [72.42530499990028]
  We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models.
  arXiv  Detail & Related papers  (2023-01-27T12:38:09Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs) This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
  arXiv  Detail & Related papers  (2021-08-27T15:04:11Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBEL is a lifted model checking approach for verifying pCTL properties on relational MDPs. We show that the pCTL model checking approach is decidable for relational MDPs even for possibly infinite domains.
  arXiv  Detail & Related papers  (2021-06-22T13:12:36Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• Safe Continuous Control with Constrained Model-Based Policy Optimization [0.0]
  We introduce a model-based safe exploration algorithm for constrained high-dimensional control. We also introduce a practical algorithm that accelerates policy search with model-generated data.
  arXiv  Detail & Related papers  (2021-04-14T15:20:55Z)
• Nonintrusive Uncertainty Quantification for automotive crash problems with VPS/Pamcrash [0.0]
  surrogate models (metamodels) allow drastically reducing the computational cost of Monte Carlo process. kernel Principal Component Analysis (kPCA) is found to be effective to simplify the model outcome description. A benchmark crash test is used to show the efficiency of combining metamodels with kPCA.
  arXiv  Detail & Related papers  (2021-02-15T16:59:39Z)
• Gaussian Process-based Min-norm Stabilizing Controller for Control-Affine Systems with Uncertain Input Effects and Dynamics [90.81186513537777]
  We propose a novel compound kernel that captures the control-affine nature of the problem. We show that this resulting optimization problem is convex, and we call it Gaussian Process-based Control Lyapunov Function Second-Order Cone Program (GP-CLF-SOCP)
  arXiv  Detail & Related papers  (2020-11-14T01:27:32Z)
• Control as Hybrid Inference [62.997667081978825]
  We present an implementation of CHI which naturally mediates the balance between iterative and amortised inference. We verify the scalability of our algorithm on a continuous control benchmark, demonstrating that it outperforms strong model-free and model-based baselines.
  arXiv  Detail & Related papers  (2020-07-11T19:44:09Z)
• Reinforcement Learning for Safety-Critical Control under Model Uncertainty, using Control Lyapunov Functions and Control Barrier Functions [96.63967125746747]
  Reinforcement learning framework learns the model uncertainty present in the CBF and CLF constraints. RL-CBF-CLF-QP addresses the problem of model uncertainty in the safety constraints.
  arXiv  Detail & Related papers  (2020-04-16T10:51:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.