Overview

The Causality Analysis in Component-based Systems project aims at the general models, methods, and applications of the analysis of root causes for adverse events—situations where a patient is harmed—in interoperable medical device systems. The goal of the analyses is to provide a precise causal relationship between the violations of individual components in the system and the violation of an overall system safety property. Based on the analysis result, better understanding of root causes is gained towards the system property violation, and subsequent recovery or prevention measures can be more guided and focused.

We take a viewpoint that it is infeasible to reproduce the scenario for the adverse event under investigation due to the time, financial cost, as well as potential harms to more patients. Instead, we seek for solutions in modeling the system under investigation and performing the analysis offline, given only the recorded trace for the adverse event and the system model. This viewpoint poses several interesting questions:

1. What is the formal definition of a cause in the context of interoperable medical devices?
2. What is the minimal set of data that must be captured for the analysis of causal relationship?
3. How would the analysis be impacted if the minimal set of data cannot be fully captured due to resource constraints on the medical devices?

To decide whether a suspected subset of faulty components is the root cause, we consider every alternative system execution trace if the suspected subset of faulty components were replaced with correct ones. According to the information available from the component contracts, such alternative system execution traces can be reconstructed. If on every such trace the system property violation is mitigated, then we claim that the suspected subset of faulty components is a cause for the system property violation. In this case, the subset is called a culprit. To solve the problem of identifying culprits efficiently, we have developed algorithms to transform the problem into an instance of checking the unsatisfiability of constructed logical formulas, and employed state-of-the-art theorem provers to assist in identifying the culprits. We have applied the approach to a case study involving the interoperability of a laser scalpel and a patient ventilatilator.

The available information on the recorded trace plays a major role in the analyzer capability to successfully identify culprits. Causality analysis generally requires accurate information on the values of the input/output ports of each of the components. To obtain such data that most current medical devices do not provide, we have implemented a prototype life data recorder (LDR) for medical devices proposed by researchers from the US Food and Drug Administration (FDA). The LDR features configurable, high frequency, secure data recording, and more importantly, minimal interference with the host medical device. The LDR works by accepting batches of “updates” from the host device and timestamping them periodically. Timing accuracy is thus slightly sacrificed for the purposed LDR features; uncertainties on event interleaving may occur, as shown in the figure below. We have defined proper notions with three-valued semantics for past-time linear temporal logic (ptLTL) to describe the uncertain recordings and conducted pilot studies on checking system properties described in ptLTL formulas on the LDR traces with recording uncertainty.

The contribution of this project is manyfold: (1) We provided the formal definition of causality between component property violations and system property violation, and developed methods for the efficient reasoning for the causality analysis. (2) We implemented a prototype version of the life data recorder recording scheme and defined proper formalism for the description of recording uncertainties.

Figure 1: Sample LDR Recording. (a) Data in compact column format. x starts with 2, and changes from 3 to 2 and to 1 in each frame. y starts with 4, and in the first frame changes to 3 to 2 and to 4, ... (b) Depicting the recording. cross for x, dot for y. (c) One possible interleaving for events that change values of x and y. (d) Another possible interleaving.

Resources

• LDR Prototype Implementation (To be relased)

Publications

• Contract-based Blame Assignment by Trace Analysis. Shaohui Wang, Anaheed Ayoub, Radoslav Ivanov, Oleg Sokolsky and Insup Lee. To appear in The 2nd ACM International Conference on High Confidence Networked Systems (HiCoNS), April 2013.
• Runtime Verification of Traces under Recording Uncertainty. Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky and Insup Lee. In 2nd International Conference on Runtime Verification, September 2011. PDF

Acknowledgements

This research is support in part by NSF CPS large grant (NSF CNS-1035715) and NSF FDA Scholar-in-Residence grant (NSF CNS-1042829). We are grateful to Paul Jones and Yi Zhang at the FDA for the motivational discussions on life data recorders and diagnosis for adverse events in medical device systems.