# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 9 Conclusions and Future Work  
We presented an MBA focused on CPN reference models of insulin infusion pump systems, aiming to assist manufacturers in assessing quality. We also described a case study on a commercial insulin infusion pump system (i.e., ACCU-CHEK Spirit). Reference models are relevant because insulin infusion pumps are safety-critical systems used to monitor and treat diabetes patients. The executable, parametric, modular, and timed CPN model included the essential features of insulin infusion pump systems to ensure correct functioning. The case study was relevant to extending the model to verify and validate two model refinements as quality assessment scenarios. Using the model checking technique, we considered the formal verification of two safety properties for the first refinement. We validated the second refinement using simulations to analyze the model concerning the commercial system's technical specifications. Finally, the empirical evaluation and the implementation of the web-based application for simulation-based training demonstrated that the \(\mathit{MBA/CPN}\) is reusable for the development and certification process of insulin infusion pump systems. Thus, the usage of \(\mathit{MBA/CPN}\) can enable manufacturers to reduce costs and development time when using formal models of insulin infusion pump systems. Manufacturers of other medical devices can also re-use it by defining and evaluating a specific reference model based on the proposed modeling steps.  
As there is a lack of studies providing generic, parametric, and timed insulin infusion pump systems models, the methods applied in this study enabled the improvement of available specifications of such systems. Thus, such a research gap also resulted in the lack of studies providing evaluations of productivity and reusability of models when reusing insulin infusion pump systems CPN models. Our study addressed such limitations improving the state-of-the art. During the empirical evaluation, time showed to be a relevant metric to measure productivity (computing the time required by each group to finish the problems that we asked modelers to solve during the evaluation phase). Two factors (understandability and adaptability) also showed to be relevant to measure reusability. Regarding formal techniques (e.g., CPN and model checking), although it is a consensus that the proposal and the use of formal methods to validate the behavior of safety-critical systems is valuable, our proposal also works as a guide, along with reusable project artifacts, for developers of insulin infusion pump systems.  
As future work, we envision conducting another empirical study to evaluate the web-based application, integrated with the reference model, to analyze if understandability and adaptability are improved. We also envision investigating the automatic generation of CPN models with a higher level of abstraction from the ACES specification. Such automatically generated models may decrease the efforts of modelers during the specification steps of our approach.  
The following are available online at [[https://bit.ly/2](https://bit.ly/2) Qyci3k]([https://bit.ly/2](https://bit.ly/2) Qyci3k), Additional Figures, Additional Examples, and Source of Models.  
All authors contributed equally to this work. All authors have read and agreed to the published version of the manuscript.  
The APC was funded by Federal University of Campina Grande.  
Not applicable.  
The authors would like to thank the Coordenacao de Aperfeicoamento de Pessoal de Nivel Superior (CAPES) and Conselho Nacional de Desenvolvimento Cientifico e Tecnologico (CNPq) for supporting this research.  
The authors declare no conflict of interest.