# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 1 Introduction
Besides the requirements required by regulatory agencies, a large number of recalls also motivates the proposal and usage of a formal Model-Based Approach (MBA) to improve quality. However, it is known that the usage of such approaches usually increases costs and development time. To address the problem of increased costs and development time, we present an MBA of insulin infusion pump systems (named MBA with CPN--_MBA/CPN_) focusing on CPN reference models as modeling artifacts to increase confidence in system behaviors and provide quality assessments. The specification of the pump system is linked to the proposed CPN model by the definition of CPN modules that represent critical parts of such a system. We describe a case study on a commercial system, i.e., the ACCU-CHEK Spirit [14], to evaluate a reference model, as part of _MBA/CPN_, by simulations and the model checking technique, describing quality assessment scenarios. The case study is also relevant to show how manufacturers can re-use the _MBA/CPN_ during a certification process. Therefore, this research faces challenges such as (1) the integration of requirements specification and assurance cases to provide re-use and (2) the re-use of a CPN reference model in a time-effective and cost-effective manner. The proposed approach may benefit the certification process by the re-use of reference models, along with an assurance cases-based requirements specification with the Goal-Structuring Notation (GSN), in the initial phases of the developing process. The refer ence model was carefully validated to decrease the possible negative impacts of a manual specification. We also conducted an empirical evaluation with 12 interviewed modelers to evaluate the \(\mathit{MBA/CPN}\). Although a reduced number of modelers experimented with our approach, such an evaluation provided insights to improve the \(\mathit{MBA/CPN}\). This study extends the results of our previous research works [7; 8], consisting of a new main contribution: an MBA to assess the quality of insulin infusion pump systems in a cost-effective and time-efficient manner. In our previous study [7; 8], we did not address (1) the integration of requirements specification and assurance cases to provide re-use (goal-oriented requirements engineering) and (2) the re-use of a CPN reference model in a time-effective and cost-effective manner. Thus, we address the following main Research Question (RQ): is the \(\mathit{MBA/CPN}\) able to provide a cost-effective and time-efficient quality assessment of insulin infusion pump systems? The quality assessment term stands for evaluating quality attributes such as safety and effectiveness, as required by regulatory agencies. Existing related works (described in Section 3) do not provide a generic, parametric, and timed insulin infusion pump systems model to assist manufacturers in conducting detailed analyses (e.g., infusion control and common recalls) during development and certification. The \(\mathit{MBA/CPN}\) addresses this limitation, considering an executable, generic, parametric, and timed insulin infusion pump systems model, that includes infusion control and considers the FDA guidelines and reported recalls. The novelty of our proposed approach also relates to the usage of GSN assurance cases during a goal-oriented requirements engineering and the simulation-based training (not requiring the CPN/Tools) of modelers to improve reusability. Therefore, 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. We aim to assist them to improve the quality of systems using an assurance case-based specification and CPN reference models. To answer our research question, we present the case study results and the empirical evaluation of models. The article is structured as follows: Section 2 presents the fundamental concepts of GSN and CPN.