Formal Verification of Voting Algorithms for Safety Critical Systems Using Two Approaches
Ranjani Krishnan, Ashutosh Gupta, Nitin Chandrachoodan, V.R. Lalithambika · 2024
For human-rated launch vehicle missions and other safety critical systems, redundancy is normally provided for inputs and outputs. To select one data from the multiple systems, a voter is needed. In this work, two voting algorithms, averaging and relative divergence were implemented in Ada and formally verified using two different tools – SPIN model checker and LLVMBMC static analyser. It was seen that the performance of the relative divergence based voter is better in some cases. Although the error scenario is remote, relying solely on self-check of the input system for data selection causes the error in averaging. The major contribution in this work is the definition of a systemic procedure for formal verification of safety-critical embedded software in Ada language with custom specifications, using two approaches. The techniques were applied to a practical case study, the voting algorithms for a safety-critical launch vehicle and found to be effective in error detection.