# Formal Algebraic Model of an Edge Data Center with a Redundant Ring Topology
## 6 Formal Algebraic Model  
In order to obtain a formal algebraic model of both the processing hierarchy and the resource migration between a couple of physical hosts, no matter whether the virtual resource is a broker or an orchestrator, it is to be mentioned that an abstract process algebra called Algebra of Communicating Processes (ACP) may be seen as a convenient solution, as it allows to just focus on relationships among objects, thus leaving aside the real nature of them [72]. It is to be said that ACP employs two atomic actions, such as send a message and receive a message, both having a generic content \(d\), so as to express the behavior of objects, which is exhibited by means of algebraic expressions [73]. It is said that a bunch of atomic actions may become interrelated among them by means of operators [74]. One of the most commonly used is the sequential, which is a binary operator and is described as \(\cdot\), whose meaning is that the first action is run, and in turn, the second action. Another common operator is the alternate, which is also a binary operator and is denoted as \(+\), meaning the execution of either the first or the second action. In addition, the merge operator admits a string of actions and is exposed as \(||\), meaning the concurrent execution of all related actions. Moreover, the conditional operator presents a condition between two triangles pointing outwards, where the action on the left must be run if the condition is true, or otherwise, the action on the right must be executed in case it is false, thus following the scheme (True \(\triangleleft\) condition \(\triangleright\) False). Those four operators are usually enough to algebraically describe the behavior of each object involved [75]. Furthermore, the encapsulation operator over a set \(H\) containing all internal atomic actions, described as \(\partial_{H}\), brings those internal atomic actions to deadlock, whilst allowing internal communications to occur. After the application of this unary operator, a sequence of events is represented where all objects involved play their part. At that point, the abstractor operator over a set \(I\) containing all internal communications, denoted as \(\tau_{I}\), masks internal communications, thus leaving only external atomic actions to happen. After applying that unary operator, the external behavior of the model gets unveiled, as the model is now presented as a black box, where only entries and exits are viewed. Then, the external behavior of the real system is obtained, and afterwards, both external behaviors are confronted in order to check whether those share the same string of actions and the same branching structure, which leads to consider the model as rooted branching bisimilar to the real system, such that a rooted branching bisimulation equivalence relation between them both is established, which is a sufficient condition to obtain a verified model [76]. Therefore, the first step to obtain the intended formal algebraic model for the processing hierarchy is to quote the behavior of each of the objects involved in the system, as shown in Table 1. In order to keep the scenario as simple as possible, let us suppose just one fixed pole within each of the quadrants and only a drone moving around, where all those types of end devices simply have one sensor and one actuator, such as the former reads raw data from the environment and passes them on to an end device and the latter receives processed data from an end device and act in the environment according to those data. When an end device receives raw data, it sends those to its broker, which either may process them and forward them to the proper actuator, or otherwise, pass them on to the orchestrator, which gets raw data transformed into processed data after undertaking the duly processing, and at that point, such data are sent back to the appropriate broker, which in turn, it sends them back to the proper end device.