# A Strategy-Based Formal Approach for Fog Systems Analysis
## 5 Execution and Formal Analysis
### Maude Strategy Presentation  
Maude [27] is a high-level formal specification language based on equational and rewriting logics. A Maude program describes a logical theory, and its computation implements a logical inference based on the program's axioms. A Maude module may be:  
1. A functional module implements an equational theory in an extension of order-sorted equational logic called membership equational logic. This theory is mathematically described by a pair \((\Sigma,E\cup A)\), where \(\Sigma\) is the module's signature that specifies the sorts, subsorts, kinds, and operators. \(E\) is the collection of equations (possibly conditional), and \(A\) is the set of equational attributes declared for some operators such as _assoc_ for associative, _comm_ for commutative, etc. 2. A system module that implements a rewrite theory as a triple \((\Sigma,E\cup A,R)\), where \((\Sigma,E\cup A)\) is the module's membership equational theory part, and \(R\) is a collection of possibly conditional rewrite rules. Example 3  
We illustrate a simple problem using Maude. In this problem [28], a shepherd needs to carry to the other side of a river a wolf, a goat, and a cabbage. The shepherd has only one boat with two seats for himself and another traveller. The problem in this example is that, in the absence of the shepherd s, the wolf w would eat the goat g, and  
\begin{table}
\begin{tabular}{c} \hline \hline
**Traces Projections on Agents** \\ \hline \(t_{1}\) Projection on \(a_{1},a_{2},a_{3}\) \\ \hline \((B_{0},h0)\overset{\text{obs}}{\leftarrow}(B_{0},h0)\overset{\text{mgrt}}{ \leftarrow}(B_{0},h)\overset{\text{an}}{\leftarrow}(B_{0},h)\overset{\text{int}} {\leftarrow}(B_{0},  
the goat would eat the cabbage c. Operation Initial refers to the initial situation, where it is assumed that all elements are located on the left side of the river through an equation. The rewrite rules represent how the wolf and goat eat and the different ways to cross the river. In this example, \((\Sigma_{RC},E_{RC}\cup A_{RC},R_{RC})\) is defined as: \(\Sigma_{RC}=\) (sorts as Side, operations as left : -> Side, and variables as S : Side). \(E_{RC}=\) equations as eq change (left) = right. \(A_{RC}=\) equational attributes as assoc and comm. \(R_{RC}=\) rewrites rules as rl [ shepherd - alone ] : s (S) = > s (change (S)). mod RIVER-CROSSING is sorts Side Group. ops left right : -> Side. op change : Side -> Side. ops s w g c : Side -> Group. op _ : Group Group -> Group [ assoc comm ]. op init : -> Group. vars S': Side. eq change (left) = right. eq change (right) = left. eq initial = s (left) w (left) g (left) c (left). crl [ wolf - eats ] : w (S) g (S) s (S ') = > w (S) s (S ') if S =/= S '. crl [ goat - eats ] : c (S) g (S) s (S ') = > g (S) s (S ') if S =/= S '. rl [ shepherd - alone ] : s (S) = > s (change (S)). rl [ wolf ] : s (S) w (S) = > s (change (S)) w (change (S)). rl [ goat ] : s (S) g (S) = > s (change (S)) g (change (S)). rl [ cabbage ] : s(S) c (S) = > s (change (S)) c (change (S)). endm  
The Maude language has been cited in many scientific articles and books. It has been used to formally specify and execute context-aware systems [29], cloud systems [30], supply chain management [31], and cyber-physical systems [32]. It is known that various extensions of Core Maude have been proposed such as HiMaude [33], to deal with hybrid systems, and RT Maude [34] for real-time systems. Among these extensions, the Maude strategy extension [12] is a specific strategy language for Maude that aims to separate the rewrite rules R and their execution using strategies. The definition of the system module becomes \((\Sigma,E\cup A,S(R,SM))\) with \(S\) the semantic describing the system's behaviour. \(S\) is defined by: \(R\) (the collection of possibly conditional rewrite rules) and \(SM\), the strategy module that is used to guide the rewrite process and the use of these rewrite rules that influences the system's behaviour.