Formal Verification of Conventionally Qualified Safety Critical Systems

Qualification of computer-based systems used in safety–critical applications is of paramount importance. Conventional/classical qualification process for such systems is based on the evidence that the system is developed following a systematic development process interfaced with concurrent independent verification and validation. Systematic review and testing help to eliminate systematic failures and establish functional correctness. It is recognized that formal verification tools, with underlying mathematically rigorous algorithms can provide supplementary evidence of correctness. However, the adoption of formal verification tools in safety critical applications and industry is still limited. This is mainly owing to two perceptions regarding formal verification—formal verification tools are not scalable, and using formal verification tools is difficult and time consuming. The formal verification tools have evolved over around two decades are mature and scalable enough to handle the programs used in safety–critical systems. These tools can be easily used with appropriate training and effort, and hence industries are now adopting formal verification to tap the advantages associated with it. This paper describes our experience on using an open source formal verification tool CBMC for verifying C programs used in a safety qualified Programmable Logic Controller. These programs were already qualified using the conventional qualification process. From the outcome of this exercise, it can be stated that formal verification techniques can be easily applied on the programs for safety critical systems (with associated systematic documentation) qualified using conventional methods.