# A Strategy-Based Formal Approach for Fog Systems Analysis
## 5 Execution and Formal Analysis
### From BiAgents* to Maude Strategy  
The defined BiAgents* specifications for the fog systems' structure can be represented by a functional module, where the declared operations and equations define constructors that build the system's elements (physical and virtual parts and their location) as shown in Table 8. Similarly, the specified BRS dynamics in addition to the agents' functions describing the system's behaviour can be specified by a system module. The different possible executions are described as conditional or non-conditional rewrite rules. In addition, each defined trace in BiAgents* may be defined by strategies composition, as defined in a Maude strategy module. As mentioned in Section 4, each reaction rule or series of reaction rules are triggered by the analysis' result of the appropriate agent. Table 8 depicts the transcription of the BiAgents* model into a Maude strategy specification. Each evolution of agents' state is represented by a simple strategy as S1 in Table 8. These strategies are a combination of sequential rewrite rules (\(observation,migration,etc.\)) \begin{table}
\begin{tabular}{c c} \hline \hline
**BiAgents* Model** & **Maude Strategy Specification** \\ \hline \hline Sorting discipline & **sorts** Agent Sensor Actuator Action DLayer ComLayer Protocol Flayer CILayer. \\ \hline \multirow{4}{*}{Reaction rules} & Conditional rewrite rules of the form: \\  & **crl** [rewrite-rule-name] : term =\textgreater{} term’ if condition. \\  & Rewrite rules of the form: \\  & **rl** [rewrite-rule-name] : term =\textgreater{} term’ \\ \hline \multirow{4}{*}{Parent function} & Operation of the form: \\  & **op** parent [\_] : Parent Child \(->\) Parent. \\ \hline \multirow{4}{*}{Agents’ behaviour} & **Virtual Structure** \\ \cline{2-3}  & **op** observe (\_) : Nat Host \(->\) System. \\  & **op** analyse (\_) : Nat Data \(->\) Pool. \\  & **op** interaction (\_) : Nat String \(->\) System. \\  & **op** mgrt(\_) : Nat Host Host \(->\) System. \\  & **crl** [**action**] : term =\textgreater{} term’ if **decision**. \\ \hline \multirow{4}{*}{Global Traces} & **Smart behaviour Traces** \\ \cline{2-3}  & **_Composed Strategy_ with operators(! ;...) \\ \cline{2-3}  & **strat** ST @ System. \\  & sd ST : = (ST1 | ST2 |... | ST9) *. \\ \hline \multirow{4}{*}{Projections} & _Defined Simple Strategies_ \\ \cline{2-3}  & **strat** ST1 @ System. \\ \cline{1-1}  & **strat** ST1 @ System. \\ \cline{1-1}  & **strat** ST1 := (S1 ;S11 ;S41 ;S411). \\ \cline{1-1}  & **S1** := (observation1 ; migration1). \\ \hline \hline \end{tabular}
\end{table} 
Table 8: From BiAgents* to Maude strategy. Example 5  
In LIS, we define the BiAgents* model with three modules (Figure 7). 1. The functional module contains five sub modules according to the agents and the four regions of the bigraphical model, named: AgentSpec, DevicesSpec, CommunicationSpec, FogSpec, and CloudSpec. 2. The system module contains two sub modules named LuggageInspectionBehaviour and PropertiesChecking. 3. The strategy module is named LuggageInspectionStrategies. The experiments were performed on a PC with an Intel(R) CoreTM i7-8650U CPU @ 1.90 GHz 2.11 GHz, with 32 GB of internal memory, and running Windows 10, version 1903 18362.900 in an Oracle virtual machine virtual Box version 6.0.14 r133895 (Qt5.6.2) 2019 windows 7 with 16 GB of internal memory. The proposed architecture is validated by the successful execution of the aforementioned system. Hence, given a starting state describing the architecture, the system always reaches the desired final state.