Formal Verification Techniques for Safety Critical Medical Device Software Control

Abstract

Safety-critical medical devices play an important role in improving patients health and lifestyle. Faulty behaviors of such devices can cause harm or even death. Often these faulty behaviors are caused due to bugs in software programs used for digital control of the device. We present a formal veri cation methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of these medical devices. Our methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) re nement, where both formal speci cations and implementations are treated as transition systems. First, we present formal speci cation model for the medical device. Second, we develop correctness proof obligations that can be applied to validate object code programs used in these devices. Formal methods are not widely employed for the veri cation of safety critical medical devices. However, using our methodology we were able to bridge the gap between two very important phases of software life cycle: speci cation and veri cation.