Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Causality for Cyber-Physical Systems

Hugo Araujo, Hana Chockler, Mohammad Reza Mousavi, Gustavo Carvalho, Augusto Sampaio

TL;DR

The paper tackles the challenge of identifying root causes of failures in cyber-physical systems by extending Halpern-Pearl actual causality to continuous, time-evolving dynamics. It defines trajectory slices and causal models for CPSs, and develops a search-based algorithm, mechanised in MATLAB/Simulink and integrated with HyConf for conformance testing. Through running examples and two empirical case studies (suspension system and connected platoon), it demonstrates how to uncover single and multi-variable causes within trajectory intervals and quantify their impact on hazards. The approach yields actionable insights for fault localization and design corrections, with benchmarks showing scalable performance and guiding practical use in CPS verification and debugging.

Abstract

We present a formal theory for analysing causality in cyber-physical systems. To this end, we extend the theory of actual causality by Halpern and Pearl to cope with the continuous nature of cyber-physical systems. Based on our theory, we develop an analysis technique that is used to uncover the causes for examples of failures resulting from verification, which are represented as continuous trajectories. We develop a search-based technique to efficiently produce such causes and provide an implementation for such a technique. Moreover, we apply our solution to case studies (a suspension system and a connected platoon) and benchmark systems to evaluate its effectiveness; in the experiment, we show that we were able to detect causes for inserted faults.

Causality for Cyber-Physical Systems

TL;DR

The paper tackles the challenge of identifying root causes of failures in cyber-physical systems by extending Halpern-Pearl actual causality to continuous, time-evolving dynamics. It defines trajectory slices and causal models for CPSs, and develops a search-based algorithm, mechanised in MATLAB/Simulink and integrated with HyConf for conformance testing. Through running examples and two empirical case studies (suspension system and connected platoon), it demonstrates how to uncover single and multi-variable causes within trajectory intervals and quantify their impact on hazards. The approach yields actionable insights for fault localization and design corrections, with benchmarks showing scalable performance and guiding practical use in CPS verification and debugging.

Abstract

We present a formal theory for analysing causality in cyber-physical systems. To this end, we extend the theory of actual causality by Halpern and Pearl to cope with the continuous nature of cyber-physical systems. Based on our theory, we develop an analysis technique that is used to uncover the causes for examples of failures resulting from verification, which are represented as continuous trajectories. We develop a search-based technique to efficiently produce such causes and provide an implementation for such a technique. Moreover, we apply our solution to case studies (a suspension system and a connected platoon) and benchmark systems to evaluate its effectiveness; in the experiment, we show that we were able to detect causes for inserted faults.
Paper Structure (40 sections, 1 theorem, 7 equations, 22 figures, 9 tables)

This paper contains 40 sections, 1 theorem, 7 equations, 22 figures, 9 tables.

Table of Contents

  1. Introduction
  2. Problem definition and contributions
  3. Structure of the paper
  4. Related work
  5. Preliminaries
  6. Causal theory for discrete systems
  7. Cyber-physical systems
  8. Running example: an autonomous vehicle
  9. Causality for CPSs
  10. Analysis of cyber-physical systems
  11. Trajectories and overriding
  12. Causal models for CPSs
  13. Causes for CPSs
  14. Practical applications of causality
  15. Causal analysis process
  16. ...and 25 more sections

Key Result

Proposition 1

In our implementation, $(M,u) \models (c \mapsfrom \vec{x})$ always holds by construction.

Figures (22)

  • Figure 1: Illustration of the running example.
  • Figure 2: Causal graph of the AT/BT example.
  • Figure 3: System trajectory.
  • Figure 4: Trajectory and trajectory projection.
  • Figure 5: Trajectory and trajectory projection.
  • ...and 17 more figures

Theorems & Definitions (24)

  • Definition 1: Signature
  • Definition 2: Causal Model
  • Definition 3: Causal Formula
  • Definition 4: Intervention
  • Definition 5: Satisfaction Relation
  • Definition 6: Cause
  • Definition 7: Valuation
  • Definition 8: Trajectory
  • Definition 9: Variables of a Trajectory
  • Definition 10: Trajectory projection
  • ...and 14 more