# A Strategy-Based Formal Approach for Fog Systems Analysis
## 4 BiAgents* Model Specification
### Smart Behaviour Modelling  
We adopt the concept of BiAgents* traces and their projections in order to model the smart behaviour of a fog system. In this section, we will consider the example of LIS system. A trace according to [26] is a sequence of bigraphs \(\langle B0,B1,...\rangle\) such that for each \(B_{i}\) and \(B_{i+1}\), there is a reaction rule \(B_{i}\to B_{i+1}\). Traces provide the different events that happen in the considered system. We note \(t=B_{0}\stackrel{{\text{R1}}}{{\sim}}B_{1}\stackrel{{ \text{R2}}}{{\sim}}B_{2}\stackrel{{\text{R3}}}{{\sim}}B_{3}\) with \(R1\), \(R2\), and \(R3\) the reaction rules that allow the transition from a bigraph to another. We represent the flow of agents in space through projection \(t^{a}\) on the agent a of a trace \(t\) defined as follows:  
\[t^{a}=(B_{i},h_{j}^{a})\stackrel{{\text{obs}}}{{\sim}}(B_{i},h_{j }^{a})\stackrel{{\text{mgrt}}}{{\sim}}(B_{i},h_{j+1}^{a}) \stackrel{{\text{R}}}{{\sim}}(B_{i+1},h_{j+1}^{a})\prec...\]  
where each \(B_{i}\) is the bigraph that holds the host \(h_{i}^{a}\). We notice that with the functions of observation (\(obs\)), analysis (\(an\)), and interaction (\(int\)), the couple \((B,h)\) does not change, because neither the structure of the bigraph nor the host of the agent changes. Conversely, the functions of migration (\(mgrt\)) and a reaction rule (\(R\)) have an effect on this couple. This study's main contribution is to give a precise interpretation to the constituent elements of a trace (structures and behaviours) and their projections. The possible events that decorate a given projection are related to agent states (Figure 6). The projection of a trace on an agent inherits this extension by enriching these projections with the functions of analysis and interaction. As shown in Table 6, each trace defines a fog system evolution that may involve one or more states \(B_{i}\in\mathbb{B}\) belonging to the physical structure \(\mathcal{B}_{F}\). For instance, the trace \(t_{3}\) indicated in Table 6 explains that, when captured data are sent to the internal protocol, the system formats this data and sends them to the fog layer. In the BiAgents* definition,the trace modelling of this behaviour implies three possible LIS states: \(B_{1}\): data are in the internal protocol; \(B_{2}\): data are formatted in internal protocol; and \(B_{3}\): data are in the corresponding fog node. The transition from one state to another is modelled by two reaction rules \(R_{2}\) and \(R_{3}\). More complex behaviour of LIS may be obtained by composing traces (operator \";\")--for example, the composed trace \(t_{1}\);\(t_{3}\);\(t_{4}\), to detect a dangerous bag in the area of luggage inspection. The system executes the trace \(t_{1}\) then \(t_{3}\) and finally \(t_{4}\). This means that first, when data are captured (\(B_{0}\)), the system sends it to the internal communication protocol (\(R1\)). Then, captured data are formatted (\(R2\)) and sent to fog (\(R3\)). Finally, the recognition system installed in the corresponding fog node triggers an action (\(R4\)) that displays an alert in the screens (\(R5\)). Similarly, other possible scenarios of LIS are as follows:  
* \(t_{1}\);\(t_{3}\);\(t_{5}\): detection of an abnormal number of bags/trays
* \(t_{1}\);\(t_{8}\): detection of hacking
* \(t_{2}\) :\(t_{6}\);\(t_{7}\): data destined to analysis
* \(t_{2}\);\(t_{9}\): detection of hacking  
Table 7 presents the different projections of the traces \(t_{1}-t_{9}\). We note that the functions host and int in our example are defined by:  
\(int(a,R1)=(``\)send to Fog\({}^{\prime\prime})\) if \(a=a_{S1}\) or \(a_{S2}\) or \(a_{S3}\);  
\(int(a,R8)=(``\)send to Cloud\({}^{\prime\prime})\) if \(a=a_{S1}\) or \(a_{S2}\) or \(a_{S3}\);  
\(int(a_{ICom},R2)=(``\)sending to Fog\({}^{\prime\prime})\({}^{\prime\prime})\); \(int(a_{ECom},R9)=(``\)sending to Cloud\({}^{\prime\prime})\).