Formal verification techniques for safety critical medical device software control

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 verification 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) refinement, where both formal specifications and implementations are treated as transition systems. First, we present formal specification 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 verification 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: specification and verification.