# A Strategy-Based Formal Approach for Fog Systems Analysis
## 6 Related Work
PEPA helps in the modelling of large-scale systems because of its characteristics of compositionality and abstraction. They evaluated the performance of their framework by stochastic simulation and fluid flow analysis. \begin{table}
\begin{tabular}{c c c c c c c} \hline \hline \multirow{2}{*}{**Approaches**} & \multirow{2}{*}{**Formalism**} & \multicolumn{3}{c}{**Modelling**} & \multirow{2}{*}{**Simulation/**Analysis**} & \multirow{2}{*}{**Genericity**} \\ \cline{3-3} \cline{5-6}  & & **Physical** & & **Virtual** & **Behavioural** & & **Analysis** \\ \hline [PERSON] et al., 2016 [35] & FAMILIAR DSL & \(\times\) & \(\times\) & ✓ & SPLOT & ✓ \\ \hline [PERSON] et al., 2021 [36] & \begin{tabular}{c} Multi-agents \\ system \\ \end{tabular} & \(\times\) & ✓ & ✓ & iFogSim & \(\times\) \\ \hline [PERSON] et al., 2020 [37] & \begin{tabular}{c} Timed \\ automata \\ \end{tabular} & \(\times\) & ✓ & ✓ & \begin{tabular}{c} iFogSim/ \\ UPPAAL Model checker \\ \end{tabular} & ✓ \\ \hline [PERSON] et al., 2020 [38] & \begin{tabular}{c} Process algebra \\ (PEPA) \\ \end{tabular} & ✓ & ✓ & \(\times\) & Stochastic simulation & ✓ \\ \hline [PERSON] et al., 2020 [39] & \
\begin{tabular}{c} Process algebra \\ (ROR) \\ \end{tabular} & \(\times\) & \(\times\) & ✓ & ROR & \(\times\) \\ \hline [PERSON] et al., 2019 [40] & BRS & ✓ & \(\times\) & ✓ & \(\times\) & ✓ \\ \hline [PERSON] et al., 2021 [41] & CA-BRS & ✓ & ✓ & ✓ & Maude & \(\times\) \\ \hline [PERSON] et al., 2020 [42] & Rewriting logic & ✓ & \(\times\) & ✓ & Maude & ✓ \\ \hline [PERSON] et al., 2017 [43] &
\begin{tabular}{c} High-level petri \\ nets \\ \end{tabular} & ✓ & \(\times\) & \(\times\) & \(Z3\) for SMT & \(\times\) \\ \hline This work & BiAgents* & ✓ & ✓ & ✓ & [PERSON] strategy & ✓ \\ \hline \hline \end{tabular}
\end{table} 
Table 11: Fog systems formal modelling approaches. In [39], the authors proposed an authentication scheme based on an extension of a real-or-random (ROR) model for fog computing systems. The authors offered a lightweight and secure model. They verified the security of the model proposed through an analysis using formal (ROR) and informal security analysis. The model proved to be secure and lightweight. However, this approach does not show well the behaviour of the system through a simulation. In [40], the authors modelled a self-adaptive fog system using the formal modelling approach of Bigraphical Reactive Systems (BRS). They modelled a fog system's structure and behaviour with axiomatic construction rules to describe the physical distribution of a fog system's elements and reaction rules to model their evolution. They also considered the formal verification of the behaviour's correctness. The authors of [43] considered different security protocols used in fog and IoT networks for data security. They used High-Level Petri Net (HLPN) for modelling physically and behaviourally their system and a Z3 constraints solver for an automated satisfiability modulo theories (SMT) solution and formal verification. They picked the Shibboleth security protocol after its analysis in the cloud-IoT environment. Considering the substantiality of this protocol's properties, the authors added new layers of Shibboleth among clients and fog nodes. Their purpose was to make authentication, authorisation, user's privacy, and data access secure from Service Providers (SP). In [41], the authors proposed a fog architecture for a fog system, an oil and gas refinery plant. They used Bigraphs to model the physical view of this system and control agents for the virtual view. The behaviour of this system was studied through bigraphical reaction rules and control agents' behaviour; the resulting model was simulated using a Maude-based tool for specified CA-BRS. They used Bigraphs and agents to model a specified fog system. In [42], the authors modelled a fog system focusing on the orchestration of the resources aspect using the rewrite logic-based Maude language. They came up with a set of monitoring predicates and atomic adaptive operations.