PakistanUS 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 Project summary 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 softwarerelated malfunctions of infusion pumps to decrease morbidity and mortality. Progress Reports
2019: 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 Class1 recalls (serious adverse health consequences or death) on infusion pumps due to software issues. Medical device objectcode software (code or the set of instructions that is executed by microcontrollers embedded in 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 objectcode verification is extremely hard because object code is very lowlevel, realtime, 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 higherlevel requirements/specification model. Formal Verification (FV) methods are found to be extremely effective to find cornercase bugs and provide bugfree guarantees in many domains, such as aircraft systems. We have developed several 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.
In industry, typically the safety requirements of a device are given in natural language. However, to use formal verification, the safety requirements need to be encoded as a mathematical model. Previously we had developed a process to turn these natural language requirements to mathematical models that can be used in verification. We extended this process to deal with requirements that deal with timing constraints. Infusion pumps have requirements that deal with time. For example, an alarm should go off within a time limit after an event has occurred. The updated process allows for requirements with timing constraints also to be modeled mathematically.
Data security is a big concern these days. Infusion pumps send data and store data in Cloudbased systems. These data are patient sensitive information. We have implemented and tested schemes that protect the data while the data is being stored in Cloud systems.
For verification of the control code, the mathematical model of the code and the mathematical model of the safety requirements look very different. But, these models have to be compared for verification. To address this gap, a function has to be developed that allows these models to be compared. Often, this function has to be developed manually. We have studied various scenarios and have developed these functions for these scenarios. Our goal is that based on these studies, we can develop a process to automate the synthesis of these functions.
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 Class1 recalls (serious adverse health consequences or death) on infusion pumps due to software issues. Medical device objectcode 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 objectcode verification is extremely hard because object code is very lowlevel, realtime, 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 higherlevel requirements/specification model. Formal Verification (FV) methods are found to be extremely effective to find cornercase bugs and provide bugfree guarantees in many domains, such as aircraft systems. We have developed five highlevel 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.
