A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset

TL;DR

This paper introduces a formal verification method to identify critical variables in control software that could cause safety violations due to single event upsets, aiming to improve safety and reduce hardware costs.

Contribution

It presents a novel algorithm combining program analysis and formal verification to accurately identify conditionally relevant variables, reducing false positives compared to traditional static analysis.

Findings

CRVs are fewer than static analysis suggests

The algorithm accurately identifies relevant variables

Potential for reducing controller chip costs

Abstract

We present a method based on program analysis and formal verification to identify conditionally relevant variables (CRVs) - variables which could lead to violation of safety properties in control software when affected by single event upsets (SEUs). Traditional static analysis can distinguish between relevant and irrelevant variables. However, it would fail to take into account the conditions specific to the control software in question. This can lead to false positives. Our algorithm employs formal verification to avoid false positives. We have conducted experiments that demonstrate that CRVs indeed are fewer in number than what traditional static analysis can detect and that our algorithm is able to identify this fact. The information provided by our algorithm could prove helpful to a compiler while it does register allocation during the compilation of the control software. In turn, this could cause significant reduction in the cost of controller chips.