Assessing traditional verification's effectiveness on safety-critical software systems

Because of the rapid growth of computer-related technologies, various organizations are putting higher demands on software systems. These include placing software in total or partial control over critical system functions such as navigating planes, controlling traffic systems, identifying military targets, and facilitating medical treatments, to name just a few. Unfortunately, certain faults in such systems can result in catastrophic consequences such as death, injury, or environmental harm. To detect these faults, various standards state that these software systems must undergo verification by specific verification techniques, both static and dynamic. However, some of these techniques are traditional in nature and do not focus on detecting safety-critical faults. Instead, these traditional techniques focus on all classes of faults. To determine the effectiveness of such techniques at detecting safety-critical faults, we conducted an experiment that measured hazardous-fault leakage (i.e., the number of safety-critical faults that these traditional techniques failed to detect). This article discusses this experiment, presents the results, and proposes some new ideas that show promise at reducing hazardous-fault leakage. Additionally, this article discusses traditional verification and how it is inadequate for verifying safety-critical software systems.