# A Strategy-Based Formal Approach for Fog Systems Analysis
###### Abstract  
Fog systems are a new emergent technology having a wide range of architectures and pronounced needs making their design complex. Consequently, the design of fog systems is crucial, including service portability and interoperability between the various elements of a system being the most essential aspects of fog computing. This article presents a fog system cross-layer architecture as a first step of such a design to provide a graphical and conceptual description. Then, a BiAgents* (Bigraphical Agents) formal model is defined to provide a rigorous description of physical, virtual, and behavioural aspects of Fog systems. Besides, this formalisation is implemented and executed under a Maude strategy system. The proposed approach is illustrated through a case study: an airport terminal Luggage Inspection System (LIS) while checking the correctness of its relevant properties: the portability of data and their interoperability. The integration of the Maude strategies in the rewriting of Fog system states made it possible to guide the execution of the model and its analysis. fog systems; BiAgents*; LTL analysis; Maude strategy +
Footnote †: journal: Future Internet  
0000-0001-5227-34X][PERSON]  
0000-0001-5227-088X][PERSON]  
0000-0001-5227-088X]N. B. * Mobility: One of the most significant features of fog systems is their capacity to connect directly to mobile devices, allowing mobility technologies. * Interactions: Instead of the batch processing used in the cloud, fog systems enable real-time interactions between fog nodes. * Heterogeneity: Different manufacturers create fog nodes or end devices, which come in a variety of types and must be installed according to their platforms. * Interoperability: Fog components may interoperate with one other and perform across different domains and service providers. The management and coordination of such heterogeneous and geographically widespread IoT devices, as well as the selection of appropriate resources, is incredibly challenging. Moreover, IoT devices have the capacity to evolve and dynamically modify their workflow composition. The internal properties and performance of IoT devices are, thus, affected. As a result, fog nodes require intelligent and automated elements to manage this dynamicity. Such complex systems necessitate a conceptual design using the appropriate software engineering techniques. This will provide a high level of abstraction for them to address all of the aforementioned issues. In the context of fog systems engineering, formal methods are the best choice; they give the necessary rigour to describe and enforce high-level fog system specifications. In this context, the fundamental raised challenges are:  
* How to abstract this complex type of systems to deal with their heterogeneous, dynamical, geographically widespread, and intelligent aspects;
* What formalism is appropriate to design structural and behavioural aspects of fog systems;
* How to execute and analyse these formal models. It is worth mentioning that the authors in [4] distinguish two types of approaches to model and understand dynamic and unpredictable behaviour of fog systems: software architecture-based approaches and algorithm-based ones. This classification is adopted since the majority of studies in the field look at the challenges from these both sides. In fact, some works such as [5; 6; 7] focus on the physical aspects of fog systems using architectures, graphical modelling, and a formal one. Others focused on the behavioural study of fog systems, such as [8], with algorithms. The novelty of this work consists in the abstract definition of the intelligent and distributed behaviour of fog systems. We propose an incremental approach with diverse specification and analysis phases (Figure 1). By adding a communication layer containing internal and external protocols, in addition to managing agents in the fog layer of a fog system's architecture, the management of the fog system's elements is improved, and the communication between the different layers is well organised.