# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 4 Model-Based Approach
### Hardware and Software Decomposition
Manufacturers and regulatory agencies can exchange documents until a final decision about the system's certification is under evaluation. For example, the regulatory agency may ask for specific evidence before the approval of the system. We provide a more detailed description of the ACES specification, as Supplementary Materials, in the \(MBA/CPN\) repository [28]. As highlighted, assurance cases based on ACES enable manufacturers to carry out the requirements traceability and verification of regulatory requirements. However, there are elements of assurance cases that do not play a fundamental role during these activities. We formally represent ACES documents based on the most relevant assurance cases for requirements traceability. We consider only goals (<goal>) and solutions (<solution>), representing requirements and project artifacts, respectively. An ACES-based assurance case is an oriented graph \(T=(V,A)\), where \(V\) is a set of nodes related to goals and solutions, and \(A\) is a set of edges that connect nodes. Formally, it is defined as a 5-tuple of five elements \(ACES=(V_{g}\), \(V_{s}\), \(v_{r}\), \(A\), \(R)\), where  
* \(V_{g}\) is a set of nodes defined as goals;
* \(V_{s}\) is a set of nodes defined as solutions such that for all \(v_{s}\in V_{s}\) its degree is 1;
* \(V_{g}\cup V_{s}\) is a set of nodes \(V\) of an acyclic connected graph \(T\) such that \(V_{g}\cap V_{s}=\theta\);
* \(A\subseteq V_{g}\times V_{g}\cup V_{g}\times V_{s}\) is a set of edges of an acyclic connected graph \(T\);
* \(v_{r}\in V_{g}\) is a specific node named the root; and
* \(R\) is a function \(R:V_{g}\cup V_{s}\to 2^{D}\) (\(D\) are descriptions of nodes). Each node \(v\) relates to a set \(R(v)\) of descriptions (e.g., source of requirements). Figure 3 illustrates the relationship between manufacturer and regulatory agency using the \(MBA/CPN\). The manufacturer and regulator access two repositories: CPN Models Repository and Evidence Repository. They maintain CPN modules of reference models and evidence on the fly, respectively. Manufacturers search for existing system modules under development in the repository to access and compose modules, generating specific systems versions. When there is no reference model (or module) available that fits the  
system, it is necessary to generate a new model that may be published in the repository. The regulatory agency evaluates the ACES-based assurance cases by analyzing arguments with linked evidence (published in the repository). The regulator may verify the model of the system available on the fly. For example, Figure 4 illustrates the highest level of the assurance case for the insulin infusion pump systems. The GSN element named SYSTEM-G1 represents a claim about the safety and effectiveness of the system under development. The goal relates to the context of software (SYSTEM-C1) and hardware (SYSTEM-C2). Strategies support arguments about the process (SYSTEM-S1) and product (SYSTEM-S2) requirements. The modules named SYSTEM-M1 and SYSTEM-M2 contain arguments following these strategies. Figure 5 presents a sample of the ACES document for the assurance case of Figure 4, composed of some of the basic GSN elements. Figure 4: Top level GSN assurance case of insulin infusion pump systems. Figure 3: Relationship between manufacturer and regulatory agency.