# A Strategy-Based Formal Approach for Fog Systems Analysis
## 4 BiAgents* Model Specification
### Physical Part Modelling  
**Definition 1**. : _Given a Fog system \(F\), its physical structure \(\mathcal{B}_{F}\) is specified as:_  
\[\mathcal{B}_{F}=(\mathbb{B},\mathcal{R},\ \mathbb{U},B_{0},F)\]  
_with:_  
* \(\mathbb{B}\) _is the set of bigraphs representing the fog system's states, and each bigraph represents a given state of the fog system at some point._
* \(\mathcal{R}\) _is the set of labelled reaction rules modelling the different possible transitions from a fog system state to another one. The set of labels is noted_ \(\mathbb{L}\)_._
* \(\mathbb{U}\) _is the set of actions_ \(\mathcal{R}\times V_{\mathbb{B}}\) _with_ \(V_{\mathbb{B}}\) _the set of nodes of each bigraph_ \(B_{i}\in\mathbb{B}\)_, and each action is related to a specific node belonging to_ \(V_{\mathbb{B}}\)_._
* \(B_{0}\) _represents the initial physical state of the fog system._ \begin{table}
\begin{tabular}{c c} \hline \hline
**CLA4 Fog** & **BiAgents* Specification** \\ \hline IoT layer & Region 0 \\ \hline \(\bullet\) Physical view: sensors, actuators, etc. & \(\bullet\) Place graph \\ \(\bullet\) Interactional view: connexions with communication layer & \(\bullet\) Link graph \\ \hline Communication layer & Region 1 \\ \hline \(\bullet\) Physical view: protocols, etc. & \(\bullet\) Place graph \\ \(\bullet\) Interactional view: connexions with fog layer and cloud layer & \(\bullet\) Link graph \\ \hline Fog layer & Region 2 \\ \hline \(\bullet\) Physical view: Fog nodes, routers, etc. & \(\bullet\) Place graph \\ \(\bullet\) Virtual view: agents, process, etc. & \(\bullet\) Agents (observe, analyse \\ \(\bullet\) Interactional view: connexions with the other layers and & control, migrate) \\ communications between agents & \(\bullet\) Link graph \\  & and agents (interaction) \\ \hline Cloud layer & Region 3 \\ \hline \(\bullet\) Physical view: Cloud systems, apps, etc. & \(\bullet\) Place graph \\ \(\bullet\) Interactional view: Connexions with the other layers & \(\bullet\) Link graph \\ \hline \hline \end{tabular}
\end{table} 
Table 2: CLA4 Fog and BiAgents* correspondences. * _F is the transition function that the model uses to reach a new state._  
Example 1  
We return to the case of Luggage Inspection System (LIS). We illustrate the previous notations to define graphically the initial state \(B_{0}\) of \(\mathcal{B}_{F}\) as shown in Figure 5. In addition, Tables 2 and 3 associate to each element of the physical part of the fog system the equivalent semantics in the bigraph model. The bigraph is composed of four regions. Each region represents a layer of the CLA4 Fog. 0: IoT layer, 1: Communication layer, 2: Fog layer, and 3: Cloud layer. Sorts are used to distinguish node types for structural purposes and constraints. For instance, some nodes must have a specific parent so that it is consistent with the fog paradigm, while controls identify states and parameters a node can have. We categorise the elements of LIS as follows: input devices' interfaces are all of sort \(i\); output ones are of sort \(k\); captured data are of sort \(e\); fog nodes are of sort \(f\); communication protocols are of sort \(c\); formats are of sort \(o\); cloud services are of sort \(a\); and instructions are of sort \(x\). The initial state of the system is modelled by a bigraph \(B_{0}=(V,E,ctrl,prnt,link):I\to J\) with \(V\) being the set of all the nodes; \(E\) is the set of all the hyperedges; the \(ctrl\) function represents the number of ports of each node; and the \(prnt\) one associates to each node a parent node or a parent region (Figure 5). The link function connects each node port to a hyperedge. For example, \(e_{1}\) is linked to the unique port of \(o_{1}\) and to the second port of \(s_{1}\). \(I\) is the internal interface of \(B_{0}\) ( number of sites, set of inner names ) \(=\langle 1,\emptyset\rangle\), and \(J\) is the external interface \(\langle\) number of regions, set of outer names\(\rangle=\langle 4,\emptyset\rangle\).