# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 1 Introduction  
The treatment of diabetes usually requires the usage of insulin infusion pump systems. Hardware components compose the infusion pump that simulates the pancreas' behavior, while software components are related to the embedded software used to control the pump [1]. As a safety-critical system, manufacturers should analyze the behaviors of insulin infusion pump systems to provide, at least, the minimum required guarantee of correctness [2]. Formal methods [3] play a significant role in verifying systems requirements and guaranteeing developed systems' correctness, reliability, and safety. In the medical domain, regulatory agencies, such as the United States Food and Drug Administration (FDA), need effective means to evaluate the devices to certify the developed systems and assure each system's safe behavior [4, 5]. Regulatory agencies are striving for rigorous techniques and methods to provide safety assurance. Formal methods can help develop dependable,safe, and secure systems and provide sound evidence for the required features to certify dependable medical systems. In this article, we used Coloured Petri Nets (CPN) formal method [6] for modeling and validation of insulin infusion pump systems. CPN is a formal graphical language for modeling and validating systems in which concurrency plays a major role. CPNs have been successfully applied for the formal specification, analysis, and verification of different communication protocols, embedded systems, and data networks, among other systems. Handling formal methods usually requires expert knowledge and increased costs and development time, which is one of the main motivations to conduct this study. Reusable reference models have the potential to reduce the impact of such costs. In a previous research work [7], a reference model to assist the certification of biomedical systems using CPN has been introduced, by specifying hardware and software components and applying simulations and the model checking technique. In another similar previous research work [8], a reference model to assist the certification of insulin infusion pump systems using CPN has also been introduced. In such research works, we showed the relevance of using a CPN reference model to generate evidence for certification. A limitation of these previous study is the lack of evaluation of the model considering reusability and productivity, reducing confidence in the capability of decreasing costs and development time in practice. Regulatory government agencies require manufacturers to demonstrate that insulin infusion pump systems do not put users in hazard situations [9]. In 2010, the FDA released the infusion pump improvement initiative [10], concerning problems such as software defects, inadequate Graphical User Interfaces (GUI), and mechanical or electrical failures. As a result, the FDA released in 2014 a guidance for industry and FDA staff to follow during the pump's life cycle [11]. According to the same guideline, the most commonly reported problems of infusion pumps include software error, human factors, broken components, battery failure, alarm failure, and over infusion and under infusion. Some of the reported problems are related to the design activity, while others are described by manufacturers as unknown problems, making it difficult to achieve solutions. There still exists a large number of recalls reported by regulatory government agencies regarding insulin infusion pump systems [12]. [PERSON] et al. [13] state that from the 70 infusion pump recalls released by FDA between 2001 and 2017, 17 recalls were caused by software failures. To address this problem, regulatory agencies have increased the surveillance stringency when manufacturers submit the system under development to the certification process. Manufacturers usually present a set of quality evidence about systems based on prescriptive standards (e.g., ISO 14971) and quality attributes.