Pakistan-US Science and Technology Cooperation Program |
Phase 7 (2017 Deadline)
Formal verification methodologies and tools to ensure safety of control software used in infusion pumps
US Partner: Sudarshan Srinivasan, North Dakota State University
Pakistan Partner: Sana Shuja, COMSATS Institute of Information and Technology
An infusion pump is a medical device that delivers fluids, such as nutrients and medications, into a patient’s body in controlled amounts. Infusion pumps are in widespread use in clinical settings such as hospitals, nursing homes, and in the home. This project aims to reduce software-related malfunctions of infusion pumps to decrease morbidity and mortality.
2018: The project targets the safety of software used in infusion pumps, which are medical devices used to deliver medications or hormones in controlled doses into the patient’s body. Typical medications delivered are insulin, opioids, and cancer drugs. Safety is a critical issue with infusion pumps because overdoses of such medicines can be very harmful or even fatal. Since 2001, the FDA has issued 54 Class-1 recalls (serious adverse health consequences or death) on infusion pumps due to software issues. Medical device object-code software (code or the set of instructions that is executed by the device) is validated using testing methods. However, extensive testing does not guarantee the absence of software anomalies (bugs) in infusion pumps, as is evidenced by the numerous FDA recalls. Medical device object-code verification is extremely hard because object code is very low-level, real-time, interrupt driven, and extensively exhibits the phenomenon of stuttering. Stuttering means that the device executes millions of microprocessor instructions to account for only a single progression of a higher-level requirements/specification model. Formal Verification (FV) methods are found to be extremely effective to find corner-case bugs and provide bug-free guarantees in many domains, such as aircraft systems. We have developed five high-level techniques in this reporting period to enable formal verification of infusion pump object code verification. The techniques can possibly also be applied to other control applications.
The first is called dynamic stuttering abstraction. As stated earlier, one of the critical challenges with verification is the complexity of object code. The mathematical model corresponding to the object code has typically millions or more transitions. We observed that many of these transitions are stuttering transitions. We found that the information contained in sequences of stuttering transitions can be compiled together and the size of the sequence can therefore be reduced. This technique is called dynamic stuttering abstraction. We found in practice that dynamic stuttering abstraction results in significant reductions to the size of the object code mathematical model.
The second technique is called static stuttering abstraction. It is the same idea as before, but applied to the object code program itself and not to the mathematical model of the object code. Application of this technique requires that we can identify sequences of instructions in the program that are stuttering and can therefore be combined.
The third technique is a method for liveness verification. This method checks for deadlock errors that often cause the program to get stuck and not make progress. Deadlock errors result in cycles of stuttering transitions in the mathematical model of the object code. Therefore, we used standard algorithms with some optimizations to check for stuttering cycles in the mathematical model of the object code. We also developed some relevant theory to make this technique applicable.
The fourth objective achieved was that we developed algorithms to then verify the abstracted mathematical model of the object code. We implemented and tested these algorithms for efficiency and found that they work well in practice. The fifth technique is a method to develop formal specifications. In formal verification, the object code to be verified has to be compared with a specification model that defines the correct behavior of the system. However, in practice, the behavior of the system is described as natural language requirements. The goal of this technique is a methodology to process these natural language requirements and synthesize formal mathematical specification models that can be used for verification.