# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 2 Preliminaries
### Coloured Petri Nets and Access/CPN  
We present a partial formalization of a CPN (elements and structure) because it is linked to different requirements in an assurance case-based specification using GSN. Thus, a CPN model is composed of elements such as places, transitions, data types, and hierarchy. A coloured Petri net module is a tuple \(CPN_{M}=(P,\,T,\,A,\,\Sigma,\,V,\,C,\,G,\,E,\,I,\,T_{sub},\,P_{port},\,PT)\):  
1. \(P\) is a finite set of places.
2. \(T\) is a finite set of transitions such that \(P\cap T=\theta\).
3. \(A\subseteq P\times T\cup T\times P\) is a set of directed arcs.
4. \(\Sigma\) is a finite non-empty set of colors.
5. \(V\) is a finite set of typed variables such that \(Type[v]\in\Sigma\) for all variables \(v\in V\).
6. \(C:P\rightarrow\Sigma\) is a color set function that assigns a color set to each place.
7. \(G:T\to EXPR_{V}\) is a guard function that assigns a guard to each transition \(t\) such that \(Type[G(t)]=Bool\).
8. \(E:A\to EXPR_{V}\) is an arc expression function that assigns an arc expression to each arc \(a\) such that \(Type[E(a)]=C(p)_{MS}\), where \(p\) is the place connected and MS refers to \"multiset\". to the arc \(a\).
9. \(I:P\to EXPR_{\theta}\) is an initialisation function that assigns an initialisation expression to each place \(p\) such that \(Type[I(p)]=C(p)_{MS}\).
10. \(T_{sub}\subseteq T\) is a set of substitution transitions.
11. \(P_{port}\subseteq P\) is a set of port places.
12. \(PT:P_{port}\to IN,OUT,\,I/O\) is a port type function that assigns port types to places. Therefore, a hierarchical coloured Petri net is a four-tuple \(CPN_{H}=(S,\,SM,\,PS,\,FS)\):  
1. \(S\) is a finite set of modules. Each module is a Coloured Petri Net Module \(s=((P^{s}\,\,T^{s}\,\,A^{s},\Sigma^{s}\,\,V^{s}\,\,C^{s}\,\,G^{s}\,\,E^{s}\,\,I ^{s}),\,T^{s}_{sub},\,P^{s}_{port}\,\,PT^{s}\,). It is required that \((P^{s_{i}}\cup T^{s_{i}})\cap(P^{s_{j}}\cup T^{s_{j}})\) = \(\theta\) for all \(s_{i},s_{j}\in S\) such that \(i\
eq j\).
2. \(SM:T_{sub}\to S\) is a _submodule_ function that assigns a submodule to each substitution transition, requiring that the module hierarchy is acyclic.
3. \(PS\) is a port-socket relation function that assigns a port-socket relation \(PS(t)\subseteq P_{sock}(t)\times P_{port}^{SM(t)}\) to each substitution transition \(t\), requiring that \(PT(p)=PT(p^{\prime}),C(p)\) = \(C(p^{\prime})\) and \(I(p)\langle\rangle\) for all \((p,\,p^{\prime})\in PS(t)\) and all \(t\in T_{sub}\).
4. \(FS\subseteq 2^{P}\) is a family of non-empty fusion sets such that \(C(p)=C(p^{\prime})\) and \(I(p)\langle\rangle=I(p^{\prime})\langle\rangle\) for all \(p,\,p^{\prime}\in fs\) and all \(fs\in FS\).  
The CPN/Tools software is used to model, conduct simulations, and run \(\text{CPN}/\text{ML}\) codes. However, it is possible to handle CPN models without requiring the usage of a GUI. The Access/CPN framework enables users to handle model components, simulations, and CPN/ML code using the Java programming language [16]. For instance, such a framework provides methods to fire the enabled transitions and obtain tokens related to specific places. This type of functionality is relevant, for instance, to embed the CPN models in software applications for training modelers on how to re-use the \(\text{MBA}/\text{CPN}\).  
Figure 1: The main components of GSN: Goal, Solution, Strategy, Context, Justification, Undefined, SupportedBy, and InContextOf.