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   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 software-related malfunctions of infusion pumps to decrease morbidity and mortality. Progress Reports 2020: 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 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 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 several techniques in this research project 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. We have developed a process to turn these natural language requirements to mathematical models that can be used in verification of object code. We also 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 process allows for requirements with timing constraints also to be modeled mathematically. The next step is to extract the mathematical model corresponding to the object code itself. The challenge here is that this model can be very large. We developed optimization techniques that ensure that the size of the models does not explode. Then we developed verification algorithms, which were implemented in a tool that check if every behavior of the model corresponding to the object code is matched by a behavior of the requirements model and vice versa. One challenge here is that 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 called a mapping function. Often, this function has to be developed manually. We developed a process that aides in the development of the mapping functions. Another issue with control code is deadlock errors, i.e., if the code is not designed carefully, it can get into situations where it gets stuck and does not make progress. We also developed techniques to detect deadlock errors in object code corresponding to infusion pumps. Data security is a big concern these days. Infusion pumps send data and store data in Cloud-based 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. 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 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 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 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 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 Cloud-based 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 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.