|Causality Analysis in Comopnent-based Systems|
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:
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.