# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 8 Discussion  
The \(MBA/CPN\) has characteristics that were not entirely considered by previous studies, such as assurance case documentation for goal-oriented requirements engineering (ACES documents), configuration (model instantiated for different systems), scheduling (constraints of infusion systems), hierarchy (management of specification complexity), and execution (simulation of behaviors). The documentation of requirements using ACES-based assurance cases helps manufacturers provide arguments and evidence for certification, reusing the same document to manage requirements. This is also relevant to decrease development time, considering that government regulatory agencies (e.g., the FDA) recommend submitting assurance cases of insulin infusion pump systems during the certification process. Manufacturers and regulatory agencies can exchange the ACES document to improve the quality of insulin infusion pump systems. Besides, to apply the \(MBA/CPN\) at a real scenario using a specific system, manufacturers only need to configure input parameters of the reference model to represent the basic required functionalities of insulin infusion pump systems. If new functionality is required for the system, the reference model's module structure provides an easy mechanism for adaptations. The reference model's re-use is the basis for developing a new system or conducting quality assessments of existing ones, comparing the insulin infusion pump systems under evaluation and the model. Although we manually specified the CPN models due to our focus on providing a verified and validated basis for further extensions, it is also possible to automatically generate models with a higher level of abstraction (first system refinement - abstract reference model of Figure 2) by inferring them from the ACES specification. The automatic generation of CPN models may be relevant if manufacturers wish to include new goals for the insulin infusion pump systems under development or wish to re-use our approach for other critical systems. The formal model is a project artifact used to conduct verification and validation activities to increase confidence in insulin infusion pump systems. The verification is relevant to conducting quality assessments of quality attributes during a certification process. The quality assessment may be conducted by comparing each module of the verified reference model with each module of the insulin infusion pump systems under evaluation. The validation is relevant to conducting quality assessments of both safety and effectiveness of insulin infusion pump systems. For example, when a recall is reported, the reference model may assist manufacturers in evaluating the system by comparing outputs with model simulation results. This can decrease cost and development time by promptly correcting the defects/failures. Considering the FDA guideline related to the life cycle of infusion pumps [11], the reference model complies with the most common reported recalls of infusion pumps, including software error and over infusion, and under infusion. Additionally, based on the same FDA guideline, the model complies with the basic requirements of infusion pump systems: infusion delivery mechanism, drug reservoir, bolus mechanism, real-time clock, pump log, and selection of therapy. Therefore, manufacturers can re-use the \(MBA/CPN\) to develop insulin infusion pump systems that comply with the main FDA requirements, correct known problems, and identify and correct unknown problems reported by regulatory agencies as recalls. However, it is essential to highlight those other relevant characteristics of infusion pumps that are not in the scope of \(MBA/CPN\), such as hardware failures, hardware degradation, communication interfaces, power supply, and electrical requirements. During the empirical evaluation, the task of representing a specific system, the ACCU-CHEK Spirit, lasted only for a few minutes, indicating that extending the modeling is not time-consuming.