# A Strategy-Based Formal Approach for Fog Systems Analysis
## 3 Motivating Case Study  
In order to ensure public safety, video cameras are used in several places of daily life: car parks, large buildings, and various public and private spaces. With the help of a fog architecture, video processing is intelligently partitioned between nodes co-located with cameras and the cloud. This allows real-time tracking, anomaly detection, and the collection of information from data captured over long-time intervals. Our choice is towards modelling a video surveillance system for airport terminals. The surveillance of airport terminals permits to fight terrorism, makes a real-time surveillance for all the departments, advances video analytics, etc. Using a fog architecture, video transmission is intelligently partitioned between fog nodes, co-located with cameras, and the cloud. Figure 3 illustrates a generic configuration inspired by [19] of any airport and its possible functioning services  
Figure 2: Cross-layered architecture for fog systems (CLA4 Fog). This system should monitor safety checkpoints for congestion, criminal behaviour, confrontations, and passengers posing possible risks. Cameras in luggage-claim areas should be in position to deter fraud and to watch for potentially unsafe objects. In general, any airport may be divided into five areas (A1, A2,..., A5) of surveillance as shown in Figure 3. In this article, we propose an abstract architecture based on the fog computing paradigm for the Luggage Inspection System (LIS), which is located in area A3. This surveillance system checks:  
1. If the lines are busy (by counting the number of trays). 2. If bar codes are identifiable. 3. If the bags are acceptable; unacceptable bags are round-shaped with long straps and the ones tied with ropes. We instantiate CLA4 Fog by defining all the elements embedded in its four layers (see Table 1):  
1. The IoT layer contains three sensors: Bag scanner, Bar-code scanner, and camera in addition to one actuator: Screen. 2. The communication layer includes internal protocols that format data using the JSON format, and external protocols format data using XML. Internal protocols are responsible of the communication between layers of a system, and external ones are responsible for the communication between different systems in the network. 3. The fog layer comprises two principal fog nodes: Recognition and alert fog nodes and all the agents that are hosted initially in the fog layer, scattered in the fog nodes. In this system, we define three sensor agents \(a_{S1}\), \(a_{S2}\), and \(a_{S3}\) (a sensor agent instantiation for each sensor), one fog control agent \(a_{FC}\), two communication control agents \(a_{ICom}\) and \(a_{ECom}\) (internal and external communication), and finally one cloud control agent \(a_{CC}\). Each agent manages a physical element of the architecture making a general management of the system. Figure 3: Generic configuration of an airport and its areas of surveillance. The cloud layer is defined by a cloud node responsible for analysing data and storing it. There are different interactions between the elements of CLA4 Fog (physical and virtual). The physical elements share data in order to compute, analyse, format, or store it. Agents communicate between each other in order to orchestrate the behaviour of the system. The different sensors collect data from the physical world, and the various sensor agents \(a_{S1}\), \(a_{S2}\), and \(a_{S3}\) use this data from their interfaces then observe this data and analyse it. \(a_{S1}\), \(a_{S2}\), or \(a_{S3}\) decides whether there is an anomaly or not. If from the camera there is more or less than 10,000 trays counted, or the bar code detected from the bar-code scanner is an identifiable bar code, or a dangerous bag is detected (from the bags scanner), then there is an anomaly. The concerned sensor agent sends captured data to \(a_{ICom}\). After analysis, \(a_{ICom}\) formats captured data using the defined internal communication protocols. Then, it communicates with the \(a_{FC}\) and sends formatted data to the fog nodes.