N-version programming (NVP), a software fault-tolerance technique being used in several safety-critical industrial applications, requires development of multiple and independently developed software versions. Results produced by individual versions are compared at run-time by voters to determine the output of the NVP system. NVP is based on the fundamental assumption that majority of the independently developed versions will always produce the correct result and that such versions would fail in statistically independent manner.
However, several empirical studies have convincingly demonstrated that common mode failures can cause serious degradation in NVP system's reliability and that the assumption of independent version failure is groundless. Common mode failures refer to the cases where multiple versions fail simultaneously when executed on a given input. Unfortunately, little is known on how one can effectively detect and eliminate common mode failures when developing a NVP system.
In this thesis, we demonstrate that weakest precondition analysis, a well-known program correctness verification technique, is effective in determining input spaces causing common mode failures in different versions. Starting from the postcondition representing failure conditions, each version is executed backward and weakest preconditions are derived. Since inputs belonging to the overlapping weakest preconditions, if there are any, would cause common mode failures in NVP system, further testing and debugging effort can be made to eliminate such failures prior to the deployment of a NVP system.
Using some of the LIP versions used in previous empirical studies on NVP, we were able to detect 13 out of 18 known faults pairs causing common mode failures. These faults involved logical flaws in the program design, and five precision-related faults could not be detected by our method. Although weakest precondition analysis can be labor-intensive since they are manually applied, our results clearly demonstrate that it is effective in identifying input spaces causing common mode failures and further improving the reliability of a NVP system.
