{"paper_id":"2d46f13d-33ed-45f9-91d7-db78ea91a6aa","body_text":"Formal Modelling and Verification of Effective Probabilistic Neural Networks for Load Balancing in a Cloud Environment | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Formal Modelling and Verification of Effective Probabilistic Neural Networks for Load Balancing in a Cloud Environment Shantanu Shukla, Vibhash Yadav This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-6006596/v1 This work is licensed under a CC BY 4.0 License Status: Published Journal Publication published 15 Oct, 2025 Read the published version in Discover Computing → Version 1 posted 9 You are reading this latest preprint version Abstract Load balancing plays a crucial role in distributed and cloud computing by evenly distributing workloads across multiple servers or network resources, ensuring optimal performance and resource utilization. It improves system reliability, fault tolerance, and response time by preventing overloading and rerouting tasks from failed or underperforming resources. This paper explores advanced load balancing techniques, focusing on machine learning integration for better handling imbalanced data and task distribution. We introduce an Effective Probabilistic Neural Network (EPNN) model that selects the best cluster for load distribution. Complementing this, we propose a Round Robin Assigning Algorithm (RRAA) for task allocation and a Data Discovery Algorithm (DDA) for identifying optimal nodes or clusters. The EPNN model’s accuracy is verified through formal modeling using the Event-B tool, ensuring the correctness of the algorithm via automated and manual proof generation. This research aims to optimize load balancing in neural network environments, offering the highest probability algorithm for efficient resource management. Load balancing Cloud computing Formal modelling Probabilistic Neural Network Event-B Figures Figure 1 Figure 2 Figure 3 Figure 4 Figure 5 Figure 6 Figure 7 Figure 8 Figure 9 Figure 10 Figure 11 Figure 12 Figure 13 Figure 14 Figure 15 Figure 16 Figure 17 Figure 18 1. Introduction 1.1 General Perspective Load balancing is an important concept in distributed and cloud computing fields where the data is involved and accessed for efficient distribution of workloads or network traffic across multiple resources to ensure optimal resource utilization, maximize performance, and minimize response time [1] [2]. Load balancing is a comprehensive and essential strategy for efficiently distributing tasks, requests, or data across multiple servers, clusters, resources, or network links. Its primary goal is to prevent any single resource from becoming overloaded. By evenly distributing the workload, load balancing ensures optimal utilization of resources, resulting in enhanced system performance, greater scalability, and improved overall network reliability [3]. Different type of key concepts ensures load distribution, like resource utilization, where a loaded task or request receives the load and an overloaded task sends the load to maximize resource utilization [4]. Another fundamental concept in load balancing is fault tolerance, which ensures system reliability by rerouting requests or tasks away from failed or underperforming resources. Additionally, performance improvement plays a vital role, as effective load balancing significantly reduces response times and enhances the overall efficiency and responsiveness of the system. Different load balancing algorithms [5] determine how to distribute the traffic or tasks, like round robin, least connection, weighted round robin, sender-initiated, receiver-initiated, and many more. The balancing approach in cloud computing is an important concept because managing the load and providing services to every client is essential. Cloud computing is an essential concept in the computer science field where the cloud refers to the internet or network. It is a technology where all the tools are accessed remotely and store, manage, and access the data online rather than locally [6]. Numerous studies have been presented concerning machine learning with load balancing [7] [8]. Load balancing in machine learning refers to the practice of addressing imbalanced datasets or uneven class distributions to ensure that machine learning models perform effectively and make fair predictions. There are different methodologies like resampling techniques [9], ensemble methods, anomaly detection deep learning methods, etc [10]. The choice of load balancing technique depends on the nature of the problem, the availability of data, and the desired performance metrics. It's essential to experiment with different approaches and evaluate their impact on your specific machine-learning problem to find the most effective solution. However, there are a few papers [11] available to introduce the load balancing models in machine learning and neural networks [12] [13]. Our research work is divided into 2 types, The first part introduces how to create an effective probabilistic neural network model of load balancing [14] [15] and the second part introduces how the model will you verified and validated with the Event-B tool [16] [17]. Both parts of our research work are introduced in this paper. In this paper, we introduced the concept of round robin assigning algorithm (RRAA) for newly arrived requests, a data discovery algorithm (DDA) for finding the perfect node or cluster, effective probabilistic neural network (EPNN) for distribution of the load in the best cluster. The EPNN algorithm helps to choose the best coordinator and perform the load distribution algorithm [18] [19] in the neural network environment [20] [21]. Formal modelling [22] [23]of the EPNN algorithm [24] is necessary for checking the correctness and mathematical proof of the algorithm. Depending upon the context and machine part of the algorithm, the proof obligation is constructed by the machine and generates the proof trees and methods to identify the working of the algorithm is working correctly. [25] These proof generation 2 types, the first one is automated, and the second one is done manually. If the event is not correctly associated with invariants or context parts, make them correct manually. This work differs from existing traditional approaches, our method combines Effective Probabilistic Neural Networks (EPNN) with formal verification using Event-B to ensure both predictive adaptability and system correctness in cloud load balancing. 1.2 Problem Statement In cloud computing environments, efficient load balancing is critical to ensure optimal resource utilization, minimized response time, and reliable load transfer between the nodes. Traditional load balancing techniques often struggle to dynamically adapt to varying workloads and unpredictable system behaviours, leading to performance bottlenecks, underutilization, or overload of computational nodes. Moreover, these algorithms lack formal verification, making it difficult to guarantee correctness and reliability in real-time cloud systems. This research paper addresses these limitations by proposing a formally verified Enhanced Probabilistic Neural Network (EPNN) based load balancing algorithm. The problem lies in designing a load balancing solution that not only adapts to real-time fluctuations using intelligent prediction models but also ensures correctness and fault tolerance through formal methods. The proposed work aims to model, implement, and formally verify the EPNN approach using Event-B and the Rodin tool, ensuring both high performance and provable reliability in dynamic cloud environments. 1.3 Research Motivation Cloud computing offers scalability, flexibility, and on-demand access to computational resources. However one of the determining challenges in the cloud environment is efficient load balancing, which ensures that the load of the servers is evenly distributed across the servers to maintain performance and optimize resource usage. A traditional load balancing algorithm that adapts to rapid workload fluctuations and uncertain resource availability. Recent advancements in machine learning, particularly Probabilistic Neural Networks (PNNs), offer promising capabilities for predicting and managing dynamic workloads through intelligent decision-making. Yet, despite their predictive power, such models are rarely integrated with formal methods that can ensure correctness, consistency, and reliability. By developing an enhanced PNN-based load balancing algorithm and formally modeling it using Event-B in the Rodin platform, this work aims to deliver a solution that is not only intelligent and adaptive but also mathematically verified for correctness. 1.4 Organization of Paper The organization of the paper is as follows: Section 2 introduces the background of the load balancing algorithm, effective probabilistic neural network, and formal modelling. Section 3 briefly outlines the related work. Section 4 described the working of the proposed effective load balancing algorithm with an effective probabilistic neural network algorithm. Section 5 presents the Event-B model of EPNN-based load balancing. Section 6 presents EPNN Load Balancing validation with Metrics. Section 7 characterizes the result analysis of the proposed model, and Section 8 concludes the paper. 2. Background This section presents several key concepts related to the domain of cloud computing., request scheduling, load balancing, effective probabilistic neural networks (EPNN), formal modelling, and neural network algorithms. A. Cloud computing: Cloud Computing is the popular and on-demand availability of different types of resources related to the computer system, like virtual systems, including file networks, memory areas, and databases. Cloud Computing operates with a service model that is divided into 4 layers. The top layer shows cloud clients such as web browsers, IOT, and digital computing devices, and the second layer communicates with the software as a service (SAAS), such as email, virtual desktop, group chat, etc. The third layer provides the platform as a service (PAAS), programming languages, libraries, application runtime database et.al. The fourth layer offers Infrastructure as a Service (IaaS), providing access to virtual machines, load balancers, networks, and storage. This layer forms the foundation of cloud-based resources. The bottom layer of the cloud computing model is the deployment model, which includes various types of cloud environments such as hybrid cloud, multi-cloud, and public cloud. A large cloud provides the functionality of distributed resources over multiple servers, each of which is called a data center. Cloud Computing shares the sources and performs the work pay-as-you-go model, which reduces the burden of monthly expenses. The main advantages of cloud computing are reduction, device independence, a large set of storage, expanded availability, increased productivity, and security measures. B. Request scheduling algorithm: The request scheduling algorithm plays an important role in cloud systems. The request algorithm ensures the efficient utilization of resources, load balancing, and timely replies from servers to user requests. In this section, different types of scheduling algorithms are used in cloud systems. 1. Round Robin (RR) algorithm: This is a simple and widely used algorithm. Requests are assigned cyclically, so there are no deadlocks and starvation conditions arise. Each server gets an equal opportunity to balance the load. The advantage of the RR algorithm is that it is easy to implement and understand, but the disadvantage of this algorithm is that it does not calculate the server load or request complexity. 2. Weighted Round Robin scheduling: Like Round Robin, servers are assigned different weights based on their capacity or processing power. Servers with higher weights get more requests. The advantage of this algorithm is that more important requests are served first, and then all other requests are served based on their weights. The disadvantage of this algorithm may not be optimal for heterogeneous server capacities. 3. Least connection Scheduling: Requests are assigned to those servers that are least loaded during the transmission. Better resource utilization and maximum throughput are the main aims of this algorithm. The disadvantage of this algorithm is does not consider server performance on response time. 4. Random Scheduling: In this algorithm, requests are assigned to random servers, which does not guarantee the optimal utilization of servers. The advantage of this algorithm is simplicity and uniform distribution of requests. Disadvantages of this algorithm lack of control and a lack of proper utilization of servers. 5. Least response time scheduling: Assign requests to the servers with the shortest response time. This algorithm mainly focuses on the reduced latency of the user. The disadvantage of this algorithm is the continuous monitoring of the response time. 6. Priority Scheduling: Assign priorities to the different types of users or requests. High-priority requests are processed before the low ones. The advantage of this algorithm is allowing for the prioritization of the critical tasks. The disadvantage of this is low low-priority tasks may lead to a starvation condition. C. Load balancing: Load balancing is a critical component in distributed systems, ensuring that resources are efficiently allocated and workloads are evenly distributed among servers or nodes. It aims to optimize performance, maximize resource utilization, and prevent system overloads. Here are the key aspects of load balancing in distributed systems: 1. Equal distribution of workload: Load-balancing algorithms distribute incoming requests or tasks evenly across multiple servers or nodes. This prevents any single server from becoming overwhelmed while others are underutilized, leading to improved system efficiency. 2. Improved Performance: Evenly distributed workloads lead to improved system performance. When requests are distributed effectively, response times are reduced, and users experience faster service, which is crucial for web applications and services. 3. Scalability: Load balancing is essential for scaling a distributed system. As the system grows, you can add more servers or nodes and use load balancing to ensure that the new resources are used effectively. 4. High Availability: Load balancing also provides high availability. If one server fails, load balancers can automatically reroute traffic to healthy servers, reducing the risk of service interruptions. 5. Dynamic Adaptation: Some load balancers use machine learning and real-time data to make dynamic routing decisions. They adapt to changing traffic patterns and server conditions. D. Effective Probabilistic Neural Network: Probabilistic Neural Networks (PNNs) are a class of neural network models that are particularly effective in various pattern recognition and classification tasks. They offer a probabilistic approach to decision-making, making them valuable for both classification and estimation problems. An \"Effective Probabilistic Neural Network\" (EPNN) in the context of load balancing is an innovative approach that integrates the principles of Probabilistic Neural Networks (PNNs) with additional features and adaptations to face the challenges posed by load balancing in cloud systems. EPNNs are designed to optimize the allocation of incoming requests to servers or nodes, ensuring efficient resource utilization and timely response to user requests. E. Formal Modelling: Formal methods are techniques used to change the complex model into mathematical notation. A formal model provides a mathematical foundation for system-level modelling, verification, and validation. The advantage of formal methods is that they help ensure the correctness and safety of systems by enabling rigorous analysis of them properly. Formal modelling is particularly valuable for critical systems where safety and correctness are of utmost importance, as it allows for early detection of design flaws and verification of system behaviour against specified requirements. It provides a structured framework for system specification and verification that enhances the quality and dependability of software-based systems. F. Neural Network algorithm: Neural networks have emerged as a powerful tool in the field of machine learning, drawing inspiration from the structure and functionality of the human brain. These networks consist of interconnected nodes, referred to as neurons, that are arranged in layers. Each neuron receives inputs, processes them, and passes the information through weighted connections to subsequent layers. The output generated from this process is determined by the weights and activation functions within the network, enabling neural networks to model complex patterns and relationships in data. Initially developed for tasks such as image recognition and natural language processing, neural networks have now found extensive application in a wide range of fields. Their ability to learn from data and generalize from examples makes them highly suitable for dynamic, real-time decision-making scenarios, including cloud computing, robotics, and financial modeling. In particular, deep learning, a subset of neural networks with multiple hidden layers, has significantly enhanced the capabilities of traditional machine learning algorithms, offering improved accuracy in prediction and classification tasks. The flexibility of neural networks allows them to adapt to diverse datasets, handling non-linear relationships and high-dimensional data more efficiently than many classical algorithms. This adaptability is especially relevant in areas like load balancing and resource management in distributed systems, where complex interactions between numerous factors must be considered to optimize performance. In this context, neural networks serve as a robust framework for developing intelligent systems capable of handling the unpredictable and evolving nature of real-world environments. 3. Related Work Initially, this section introduces some previous work in the field of formal modelling with different machine learning techniques and real-time task scheduling. There are many existing works on the concept of neural networks. In a survey about load balancing with cluster coordinators using different machine learning technologies [26] [27] [28]. Formal modelling-based papers in load balancing also play an important role in my research [29] [30] [31]. In this paper, different methods of load forecasting on deep learning in cloud architecture are used. Different algorithms proposed by the author, such as the load forecasting process in Spark architecture and the data partition algorithm, explain the whole framework of the load forecasting and load classification. This paper [32] defines the load balancing strategy based on deep learning for multiple controllers in SDN to solve the load imbalance problem. The Q-values for switch migration actions are derived using a Double Deep Q-Network (DDQN), which is then trained through a replay mechanism to fine-tune and optimize the Q-network parameters. In [33] this survey paper, machine learning-based load balancing algorithm in the future heterogeneous network. This survey provides a guidelines and roadmap for developing the new load balancer models in future heterogeneous networks. Key performance indicator (KPI) used in the evaluation of load balancing models, along with load balancing the relationship between the concurrent optimization of coverage (CCO) and mobility robustness optimization (MRO). In [34] this paper is a comprehensive study of load-balancing approaches in cloud computing environments with fault-tolerant approaches. This paper also discusses the problem of load balancing in the cloud computing environment and identifies the need for a best load-balancing algorithm that combines fault tolerance metrics. Now, we have discussed some research papers that are based on neural networks, genetic algorithms, deep learning, CNN, MPSO, probabilistic neural networks, software-defined networks, and reinforcement learning. In this paper [35], the effective dynamic load balancing (EDLB) algorithms using CNN. After that, particle swarm optimization (PSO) is used for advanced modification, and results show that ELBS shows recent load balancing techniques to achieve the minimum average turnaround time (TAT) and fog resource monitor (FRM). This paper [36] presents the study of the application of adaptive load balancing implemented in ECDN servers. A neural network controller using a proportional-integral-derivative (PID) algorithm was developed to achieve near-optimal performance. In this paper [37], the author presents the significance of deep learning approaches that have been analyzed in the area of cloud computing using DLD-PLB. The paper presents the framework for workflow execution in a cloud environment that has been proposed and implemented with dynamic virtual machines and load balancing. In the paper [38] work connects the fields of machine learning and networking systems, showcasing how machine learning can be applied to network load balancers. It also highlights additional challenges that need to be addressed for the successful integration of machine learning into network systems. Another field of research work implemented in this paper is formal modelling techniques implemented in load balancing and machine learning approaches. There are different papers implemented in this field. Most of the papers are implemented in different formal verification and validation themes under SAT-SMT, theorem proving, model checking, prediction, probabilistic programs, neural networks, and many other themes. In this paper [39], the author presents the hierarchical hardness model for Boolean satisfiability (SAT), which determines the satisfiability of a Boolean set of equations for a set of inputs. This paper is implemented under the classification task of machine learning. This paper [40] presents the widely observed fact that there is no single ‘dominant’ SAT solver. This methodology takes as input a distribution of problem instances and a set of solvers, then constructs a portfolio optimizing a given objective function. A decision tree-based machine learning algorithm is implemented in this paper. In this paper [41], probabilistic programming is used in reasoning about approximation, convergence, Bayesian inference, and optimization methods to prove with formal verification techniques. This work is based on a directed acyclic graph (DAG) machine learning task and a stochastic computation graph (SCG) based machine learning algorithm. All these papers are present on formal verification and validation based on many research areas. We survey about two themes; the first survey is about the comparisons table between all ML/NN/DL oriented formal verification or validation and the second comparison is based on all ML/NN/DL oriented and load balancing algorithms. 4. Working of the Proposed effective Load balancing Algorithm with EPNN In server management, load balancing plays an important role in optimizing resource utilization, maximizing throughput, and minimizing response time. It is an extremely significant issue to achieve load balancing among the cluster and its servers and nodes. Load balancing is a technique in server management to distribute the load between servers equally to increase performance, such as fail-over, and avoid bottlenecks and scalability. The load balancer strategy proposed in this paper with a help of neural network strategy. This strategy is based on an effective probabilistic matchmaking neural network algorithm. In this algorithm, we match the load for the best server. If the best server is found, it is completed. Otherwise, we send the request again to the server manager and choose another one. After choosing the best server, we select the new coordinator, called the probabilistic neural network coordinator. The proposed architecture represents how the servers are allocated in the cloud environment and interconnected with each other. Each request can access its neighbour via wireless, and the request is saved in the dictionary, and the coordinator will choose to right server to process the load. The proposed architecture has been implemented to solve the issue related to execution time, throughput, and proper resource utilization. The EPNN-based algorithm performs the major role of sequencing, sending data, and receiving replies. This neural network algorithm used a string-matching algorithm for choosing the most efficient underloaded server. Each process has a few parameters that reflect the needed capabilities of the server, which are: 1) CPU power needed for each server. 2) Memory space needed for each server 3) Storage requirement needed for the server, which reflects the needed cache size 4) Each server needed the threshold value so that none of the servers crossed the threshold. The cloud servers can distribute the requests equally. If all the capabilities match the parameters, then the load will be transferred accordingly. Choosing the EPNN load balancing algorithm helps to highlight its innovation and effectiveness. This neural network provides the advantages of dynamic adaptability, prediction-driven decision-making, energy efficiency, and threshold-based rules. Proposed Algorithm Algorithm: EPNN-Based Load Balancing Strategy 1. Initialize Cluster Groups: C1, C2, C3 2. Receive New Request R1 3. Select Nearest Cluster: Chosen_Cluster ← NearestCluster(R1) 4. Decide Cluster Coordinator for each cluster group 5. IF R1 ∈ PreRequestTable (PRT) THEN ServerManager retrieves the required data from PRT Send data to Request R1 ELSE ServerManager checks the required capabilities of R1 IF Capabilities_Match = TRUE THEN CloudServer executes R1 Send a reply to the requester ELSE CloudManagerServer (CMS) initiates Data Discovery Algorithm (DDA) IF Capabilities_Match = FALSE AND All_Servers_Overloaded THEN CloudMasterServer selects alternate cluster: Use Round Robin (RR) to select a cluster with: - Highest Priority - Most Underloaded Coordinator Use EPNN to search CloudMasterTable for the best-fit server IF Suitable_Server_Found THEN Underloaded_Server replies and takes the load CloudManager assigns requests using RR based on capability Update Formal Model: Set Server.Pattern_Match ← TRUE ELSE Create New Node: Designate as PNN Coordinator to coordinate the load Assign searching another intermediate cluster responsibility for the load 4.1 Description of EPNN, RRAA, DDA, Event-B and Rodin tool In this paper, we introduce the machine learning-based concepts regarding the effective probabilistic neural network (EPNN), external resource access algorithm (ERAA), round robin assigning algorithm (RRAA), and data discovery algorithm (DDA). These terms help the modelling with load balancing in a dynamic environment. A) Round robin Assigning Algorithm: RR algorithm identified the cloud mastering server (CMS) for all the upcoming requests. Input: A) Cloud Architecture B) Identified cloud master server (CMS) C) Master server manager (MSM) D) Initial value in round-robin assigning table (RRAT) E) Arrival time calculating server (ATCS) F) Arrived Request (RA) Output: Arrival Time Assigning Table (ATAT) Steps of the RRA Algorithm: For each incoming request Ra: ServerManager → send Ra to TimeCalculatingServer (TCS) TCS: Calculate NewArrivalTime (NAT) using fuzzy logic based on: - Predefined Time (PT) - Deadline Time (DT) - Request Size (RS) Arrange all requests in ascending order of NAT If multiple requests have the same NAT: Sort those requests by Turnaround Time (TAT) End If Enqueue the sorted requests into PriorityQueue Send PriorityQueue to CloudMasterServer (CMS) CMS: For each request in PriorityQueue: Try to serve the request on the selected optimal server If request cannot be served: TCS → recalculate Turnaround Time (TAT) Forward the request to another cluster End If End For End For B) Data Discovery Algorithm: For each request, if the required data is not found in the local cloud cache, some steps will be performed: 1) If the required data is not available in the assigned cloud cache, the cloud master server will send the request to its neighbour using the data discovery algorithm (DDA). 2) If none of the master servers are sufficient to adjust the request, send it to another cloud master server (CMS) and send a cancel message to the other server’s node. Steps of the DDA Algorithm: For each incoming request Ra: If the data required for Ra is available in the cloud server's cache: CloudServer → perform Ra CloudServer → send reply to requester Else: ServerManager → forward Ra to another CloudMasterServer (CMS) for processing End If End For C) External Resource Access Algorithm (ERAA): If the resource is not found in the master server, then search for the resource in another cloud. Steps of the ERA Algorithm For each requesting Cloud Master Server (CMS): CMS → send data request to its neighbor CMS For each receiving neighbor CMS: If the required data is found: Neighbor CMS → send data to requesting CMS Else: Neighbor CMS → reply with \"Not Found\" message End If End For If data is not found in the neighbor CMS: Requesting CMS → send a request to another cloud to search for the resource End If End For D) Effective probabilistic neural network (EPNN) 1) Input layer: The input layer consists of nodes representing various input features or parameters related to workload distribution.For example: CPU usage, Network traffic, memory usage 2) Pattern Layer: The pattern layer is responsible for storing the pattern and relationship between the input feature and the corresponding load distribution. 3) Summation Layer: Weighted summation of the output of the pattern layer. 4) Output Layer: The output layer represents the load distribution across the available server. In this layer, the most suitable server will be chosen from all the servers after the processing in the summation layer. A matchmaking process using an Effective Probabilistic Matchmaking Neural Network (EPNN) algorithm. The goal of this process is to select the most appropriate server from a set of candidate servers based on certain conditions and then update the pattern-matching status. We will make a new PNN coordinator in place of the cluster coordinator to coordinate the load. E) Event B: Event B [42] is the formal method used in formalizing and developing systems for system-level specification design and verification. It provides a structured approach to modeling complex systems, aiding in the development of correct and reliable software. Event B method is based on set theory & predicate logic, offering a mathematical base for rigorous system analysis. Event B models are separated into two basic components: contexts and machines. The context part describes the static part of the model, whereas the machine part describes the dynamic part, where all events are formalized step by step with the help of guards and actions. Event B allows the model to be developed step by step via mechanisms such as machine refinement and context extension. Key aspects of Event B include events that represent state changes in the system, capturing the conditions under which an event can occur and the effect it has on the system state. The second aspect is refinement, where this process allows the gradual development of a system from an abstract specification to a concrete implementation. The next aspects of event b are theorems and proof obligations, this obligation ensures that the specified system properties hold at each refinement level, providing a systematic way to ensure correctness. F) Rodin Tool: The Rodin tool is a formal modeling platform designed for system development using the Event-B method. It provides a framework for creating and verifying complex systems through refinement and proof obligations. Built on an Eclipse-based integrated development environment (IDE), Rodin supports system behavior modeling using set theory and predicate logic. The tool automates the mathematical proof process, ensuring consistency across different abstraction levels. Its primary objective is to enable rigorous development of reliable and error-free software systems, making it a valuable resource for formal verification and validation [43] . 5. Event-B model of EPNN-based load balancing After introducing EPNN, ERAA, DDA, and RRAA, the Event B model of EPNN load balancing contains various invariants and events [44]. As we know, the Rodin tool has two parts- context and machines. Context’s part contains a set, constants, and axioms, where all the static parts of the model should be contained. In the sets part, we have declared the set of messages, node, coordinator, requests, status, etc. In constant part, we have declared underloaded, overloaded, request, reply, in progress, completed, etc. In the axioms part, we defined the definition of status where all type of load is declared of the node. In the case of message type, whenever it is requested, reply and minimum load. A mapping (mm↦nn) ∈ sender indicates that message mm is sent by the node nn. The machine part contains a dynamic part where variables, invariants, and events. Invariants define the definition of variables and initialize each variable in the events. Events refer to fundamental constructs used to model state transitions in the system. In the Rodin tool, events are a key component of event B models, providing a formal and systematic way to specify and analyze system behaviour. The machine part of the EPNN model like variables, invariants, and initialization as follows: Variables: clustergroup, nodegroup, sender, msgsend, messagetype, deliver, serverstatus, prerequesttable, servermanager, minloadmsg, replymsgrcd, requirementserver, selectedserver, patternmatching, clustercoordinator, PNNgroup, PNNcoordinator, nodeload, nodepriority Initialization: We declare all the initial values with ∅ a value, but some values cannot be null. Like serverstatus variable declared with an underloaded value. At the initial level, the status of the server must be declared as underloaded or overloaded. A) The variable nodegroup is a subset of the NODE set (Inv1). Similarly, clustergroup is a subset of CLUSTER set (Inv2). The variable sender sends the message from the request node shown in (Inv4). B) Inv6 shows the type of message which is request, reply, and minimum load. Inv7 similarly represents the node status timein or timeout. Variable serverstatus shows the status of the server underloaded, overloaded, and most appropriate (Inv9). C) Variable requestqueue is a bijective relation between nodes in set NODE and messages in set MESSAGE (Inv10). The receiver node receives the request message from the sender node and saves it in the request queue form of the table. D) Inv13, replymsgsend represents the sending of a message from an underloaded node to an overloaded node. E) The variable prerequesttable states that the function is a total function from the set REQUESTS to the set prereqstatus. The status of the pre-request table is already and not appropriate (NA). (Inv15) F) Inv18, replymsgrcd shows the messages received by participating nodes from the corresponding node. G) In Inv19, the statement suggests that a \"requirements server\" belongs to the set or type of nodes denoted by \"NODE,\" and it is related to or connected with a \"calculating server.\" The parameters of the calculating server are the predefined time, deadline time, and request size. H) The variable patternmatching shows that the selected server or node in the cluster matches all the requirements and provides either true or false. (Inv21) I) Inv22 and Inv24 represent the clustercoordinator and PNN coordinator, where a new node is selected in the cluster group and PNN group and declared as a coordinator. J) Variable nodeload shows the load of the node, which is a natural number (Inv25). Variable nodepriority decides the priority of the node, which are either low or high (Inv26). Variable probscore represents the probability of all the nodes (Inv27), and selectnode represents the highest probability node that will be selected (Inv28). (See Fig2) 5.1 Events In the previous section, we defined variables, invariants, and initialization of EPNN load balancing. Now we elaborate on the events in an effective probabilistic neural network process (EPNN). Events are a fundamental concept used to model the behaviour and changes in a system. Events are specified within the context of transition and modification. The initial event in the Rodin tool is typically named ‘INITIALIZATION’ and is responsible for setting up the initial state of the system. This event is automatically executed when the system starts. Create other events to capture state changes or actions within the system. These events should be defined with preconditions and postconditions, specifying the conditions under which the event can occur and the changes it makes to the system. Rodin generates proof obligations for each event, ensuring that the specified preconditions imply the postcondition and that the events preserve invariants. A) Create clustergroup: In this event, the Rodin tool event \"Create ClusterGroup\" defines the creation of a new cluster group. It selects a node from the existing nodes, removes it from the \"nodegroup,\" and adds it to the \"clustergroup,\" ensuring the selected node is valid and not already in the cluster group.Node nn was removed from node group (act1) and added to cluster group (act2) (See Fig3). B) Sending the request into cluster: In this event, \"Request will be sent into cluster\" models the process of sending a request message from a node in the \"clustergroup.\" When a node nn is selected from the cluster, and a new message mm is chosen, the event ensures that nn is a valid node, mm is not already in the set mess (grd4), and it has not been sent before by any node in the current sender domain (grd5). If conditions are met, the event updates the system state. It associates the message mm with the node nn in the sender domain (act1), sets the message type to \"request,\"(act2) updates the status of node nn to \"timeout,\"(act3), and records the message mm in the set ‘msgsend’(act4) and priority of node nn is low (See Fig4). C) Declare the coordinator: The event is triggered when a condition is satisfied, including the presence of a cluster, the availability of a new node (nn2 ), and the absence of a mapping between the current coordinator ( cc ) and the new node in the “cluster coordinator” relation. The guard 4 present that node nn2 is not declared yet as “cluster coordinator”. Node \" nn2 \" in the system model must be less than or equal to a predefined threshold value (grd5). The action updates the “cluster coordinator” relation by assigning the new node (nn2) as the coordinator for the specified cluster ( cc ). (See Fig5) D) Delivery of Request message in coordinator node: In Fig6, the node nn must be part of the set of nodes (reqnodes) that are eligible to receive requests (grd1). The status of the node nn must be set to \"timeout,\" suggesting that the node is available for receiving a request (grd4). There should not be an existing mapping from node nn1 to message mm in the deliver relation, indicating that this message has not been delivered to node nn1 before (grd11). The combination of message mm and node nn should not exist in the requestqueue nn1 relation, ensuring that the request is not already in the processing queue (grd12). We declare node nn2 is the coordinator from the previous event (grd13). The action updates the deliver relation by adding a new mapping from node nn1 to message mm , indicating that the message has been delivered to node nn1 (act1). In act2, the action updates the requestqueue relation by adding a new mapping from node nn1 to a set containing a new mapping from message mm to node nn , indicating that a new request is added to the queue of node nn1 . In act3, defines the message delivered within the time frame. E) Nearest cloud will be chosen: After delivery of the message into node nn1 , the nearest cloud is selected for processing the request. In Fig7, message mm is successfully delivered in node nn1 (grd7). Guard 8 represents the value ld must be a natural number, representing the load. The load value ld must be equal to the difference between the specified lvalue and a threshold, ensuring that the load is within a certain range (grd9). Node nn sends the message mm and saves it in the sender domain (grd10). The combination of the original request message mm and the new message m must not be in the domain of the replymsgsend relation, ensuring that this reply has not been recorded before (grd14). The new message m and its load value ld must not be in the load relation, ensuring that the load information has not been assigned yet (grd16) and the load of node nn1 must not exceed a predefined threshold (grd17). If all the guards are true, then we perform some action according to our algorithm. In act1, the msgsend relation is updated by adding the new message m to the set of messages that have been sent. We define the type of message mm as ‘reply’ and update the replymsgsend relation by adding a new mapping from the pair {mm ↦ m} to the node nn1 , indicating that this reply is sent to node nn1 (act2 & 3). Updates the sender relation by assigning node nn1 as the sender of the new message m and updates the load relation by assigning the load value ld to the new message m (act4 & 5). The priority of node nn1 is set to high. F) If the request is already predefined: In this event, the value associated with request rr in the prerequesttable relation must be \"already,\" indicating that this request has already been processed (grd6). In guard7, the combination of request rr and its associated load value rld must not be in the server manager relation, ensuring that this request has not been assigned a load value in the server manager. Load value rld must be a natural number, representing the load to the request in the server manager(grd8). If all the guards are true, then the action updates the servermanager relation by adding a new mapping from the request rr to its load value rld , assigning the load value to the request in the server manager. (See Fig8). G) Send the reply to node from server manager: In this event, the reply message received from node nn into node nn1 with message m, where the message type of m is minimum load represented with load value rld . In guard 7, the combination of the request rr and its load value ld must be in the servermanager relation, indicating that this request has been assigned a load value. The combination of the pair {m ↦ rld} and nn1 must be in the replymsgsend relation, indicating that a reply message has been sent to node nn1 containing the minimum load message rld (grd11). Node nn1 and the set {m ↦ rld} must not be in the replymsgrcd relation, indicating that this reply has not been recorded before for node nn1 (grd12). If all the guards are true, action will be pursued according to the condition. In action, this event updates the replymsgrcd relation by adding a new mapping from node nn1 to the set {m ↦ rld}, recording the reception of the reply message by node nn1 in the action field (act1). (See Fig9) H) If the request is not found in the server manager: In this event, we assume no server is found up to the mark then we send the request to other servers, that are situated in another cluster. The combination of request rr and its load value rld must not be in the servermanager relation, ensuring that this request has not been assigned a load value in the server manager (grd5). If all requirements are fulfilled like predefined time, deadline time, and request size, then send the message into that cluster or server (grd6,7,8). The combination of the pair {mm ↦ m} must not be in the domain of the replymsgsend relation, ensuring that this reply has not been recorded before and the message m must not be in the domain of the sender relation, indicating that it has not been assigned a sender yet (grd9 & 10). In the action part, the action 1 updates the replymsgsend relation by adding a new mapping from the pair {mm ↦ m} to the node nn1 , indicating that a reply message containing the pair {mm ↦ m} is sent to node nn1 . (Act 1). In Act2, updates the sender relation by assigning node nn1 as the sender of the message m and declaring the message type as a reply. (See Fig10) I) If the required capability is not matched with any server: A new request will be sent in the cluster, but none of the cluster’s servers will match the essential requirement then we will divert the request into another cluster. In Fig11, nodes nn1 and nn must represent a valid node (grd1 &2). If none of the servers is capable of serving the request, then we choose the other cluster (See guard6,7,8). If we assume node nn1 is overloaded and other nodes are also busy, choose the other one (guard 9). Variable nn2 must be a set representing a valid subset of nodes and the set of nodes represented by nn2 must not be a subset of the cluster group yet (grd10 &11). If all the guards are true, then the action updates the “nodegroup” by removing the nodes represented by nn2 from it (act1). In act2, the action updates the clustergroup by adding the nodes represented by nn2 to it and setting the priority of node nn1 as low (act3). J) Choose another appropriate cluster from all cluster groups: From the previous event, if the required capability is not matched, then choose another cluster group’s node. In this event, we assume all the requirements are fulfilled by the server’s node and it is underloaded and accepts the load, then we will transfer the load. In Fig12, the variable nn2 must represent a valid node in the system, and node nn2 must be part of the cluster group (“clustergroup”) (grd1 & 2). The requirement for the server at node nn2 must be \"predefined time, deadlinetime & requestsize is fulfilled shown in (grd5,6,7). The combination of node nn2 and message mm must not be in the deliver relation, indicating that this message has not been delivered by node nn2 yet (guard10). The combination of the pair {mm ↦ nn} must not be in the requestqueue relation for node nn2 , indicating that this request has not been queued for delivery by node nn2 (guard11). If all the guards are true, accordingly action will be performed. In Act1, updates the deliver relation by adding a new mapping from node nn2 to message mm, indicating that node nn2 delivers message mm . In acts 2 & 3, update the requestqueue relation by adding a new mapping from node nn2 to the set containing the pair {mm ↦ nn}, indicating that node nn2 queues this delivery request and updates the server status of node nn2 to \"mostappropriate\" for receiving the load and priority of node nn2 is set to high. K) Choosing the best server using round round-robin technique: To decide the best server, we choose the round-robin assignment technique. In this technique, if there is more than one request has the same arrival time value then the server manager will arrange them according to the turnaround time (TAT). In Fig13, the variable ss must represent a valid server in the system (grd1). The server status of the node nn2 must be \"most appropriate,\" indicating that this server is considered the most appropriate for the current operation in another cluster (grd2). The combination of node nn2 and the set containing the pair {mm ↦ nn} must be in the “request queue” relation, indicating that this request is queued for delivery by node nn2 (grd3). The server ss must not be in the set of selected servers, indicating that it has not been chosen in the current round-robin iteration. If all the guards are true then we choose the best server using round-robin techniques. This server must fulfill all the conditions like large request size, large predefined time, less deadline time, and less loaded one. In act1, the server ss must not be in the set of selected servers, indicating that it has not been chosen in the current round-robin iteration. L) EPNN algorithm for selecting the best node: In this event, choosing best node belongs to the set of all available nodes (grd1). This guard (grd2) states that ss, which is the currently selected server, is being checked or compared in the process. It ensures consistency with the overall system state regarding server selection. In grd3, node nn3 is less than or equal to a predefined threshold. The threshold represents the maximum load that a node can handle efficiently. Now guard 4 present the universally quantified guard condition. It ensures that for all nodes k that belong to the set of nodes (NODE), if their load is below the threshold, the probability score of node nn3 is greater than or equal to the probability score of any other node k. In other words, nn3 is selected because it has the highest probability score among all the nodes with a load below the threshold. In action, act1 updates the set selectnode by adding nn3 to it (See Fig14) M) EPMNN Algorithm: In the previous event, we select the best server using the RR algorithm. After this, we matched all the conditions. If all the patterns are matched then selected node nn2 makes them true. The \"Effective Probabilistic Matchmaking Neural Network Algorithm\" in load balancing is likely a sophisticated method that uses probabilistic matching, possibly facilitated by a neural network, to dynamically and optimally distribute computational workloads across servers in a network. The goal is to achieve efficient resource utilization, minimize response times, and enhance the overall performance of the distributed system. A neural network might be employed to dynamically adjust the assignment of tasks to servers based on real-time feedback and historical data. In Fig15, the variable ss represents a server that has been selected in the current context. The guard ensures that the server ss is indeed in the set of selected servers (grd1). The guard (grd2) checks that the server status of the node nn2 is \"mostappropriate\" indicating that this server is considered the most appropriate for the current operation. In grd3, the guard checks that the current pattern-matching status for node nn3 is set to \"probabilistic false,\" indicating that the pattern-matching process for this server is currently not activated or has not been marked as successful. In act1, action updates the pattern matching status for node nn3 by assigning the value \"probabilistic true\" to it. This signifies that the pattern-matching process for this server has been successful or activated as a result of the probabilistic matchmaking algorithm N) If a new request is not matched in the same server: If the matched server is not available in the same cluster, then we will find the next server by broadcasting the request message. The guard1 checks that the server ss is not already in the set of selected servers. This condition ensures that the server is not currently selected for the task. In grd2 & grd3 ensure that variable ss2 represents another server in the system. The guard ensures that ss2 is a valid server and checks that the server ss2 is already in the set of selected servers. This condition likely ensures that ss2 is selected for the task. Grd4 checks that the pattern-matching status for node nn2 is \"probabilistic false,\" indicating that the pattern-matching process for this server is not currently successful or activated. Guard 8 checks that the pattern-matching status for node nn3 is \"probabilistic false,\" indicating that the pattern-matching process for this server is not currently successful or activated. Grd 10 and 11 shows that specifies that the computational load of node \" nn2 \" must be equal to or greater than a predefined threshold and the computational load of node \" nn3 \" must not exceed a predefined threshold. If all the guards are true, act1 updates the set of selected servers (“selectedserver”) by adding ss2 to it. This signifies that ss2 is now selected for the task. Act2 & 3 represent that updates the nodegroup by removing nn3 from it. This likely means that nn3 is no longer available for receiving tasks and updates the clustergroup by adding nn3 . This likely means that nn3 is now part of a different cluster. Action4 & 5 update the pattern matching status for node nn3 by setting it to \"ptrue.\" This signifies that the pattern-matching process for this server is now successful or activated and it is underloaded for receiving the load of new requests. (See Fig16) O) Make a probabilistic neural network (PNN) coordinator: In Fig17, after declaring node nn3 is suitable for processing the load of new requests then we will make a PNN coordinator for handling the request. A probabilistic neural network (PNN) in load balancing operates by leveraging statistical probabilities to distribute computational tasks across servers dynamically. It learns patterns from historical data to predict optimal servers, considering factors like server load, response times, and task requirements. The network probabilistically assigns tasks to servers based on learned correlations, aiming to achieve efficient resource utilization and minimize system bottlenecks. The guard grd4 checks that the pattern matching status for node nn3 is set to \"ptrue,\" indicating that this node has successfully undergone the pattern matching process, and grd3 presents that server node nn3 has underloaded. Guard5 ensures that pp is a valid node representing a member of the Probabilistic Neural Network (PNN) group. Guard6 checks that the pair (pp ↦ nn3) is not yet declared the PNN coordinator, ensuring that the selected PNN group pp is not already a coordinator. Previously, node nn2 was the cluster coordinator (grd8). Guard9 checks that the nodes nn2 and nn3 are the same, ensuring that the selected coordinator node has the same properties as the specified node with potential PNN coordination. Guard 10 shows the server ss is the selected server. If all the guards are true, then we declare node nn3 as PNN coordinator (act1). A summary of all events ensures that the specified Rodin tool events collectively describe a dynamic and adaptive load balancing system using probabilistic techniques and neural network concepts. The events cover various aspects of the load-balancing process, addressing server selection of minimum load, pattern matching, and coordination within clusters. The \"Effective Probabilistic Matchmaking Neural Network Algorithm\" event introduces probabilistic matching, utilizing neural network principles to assign tasks to servers efficiently. Another event ensures that if a server request is not matched, alternative servers are selected based on specific criteria. Moreover, the system dynamically designates new nodes as PNN (Probabilistic Neural Network) coordinators to handle load coordination, considering underloaded status, successful pattern matching, and cluster coordination. These events collectively depict a sophisticated and adaptive load balancing mechanism that optimizes resource utilization and minimizes bottlenecks in a dynamic computing environment. 6. EPNN Load Balancing Validation with Metrics For the validation process, we applied a probabilistic neural network (EPNN) model for load balancing across multiple servers. We take a dataset of 200 rows, where the dataset includes features like server status, data progress, network traffic, server load, and priority levels. The EPNN model aims to predict the optimal server (between s1 to s7) based on these features, ensuring balanced resource distribution and minimal latency. For output parameters, we calculate the predicted server and their probability between servers. The dataset was split into training (80%) and testing (20%) subsets using the hold-out validation technique. Features were normalized using Standard Scaler for better performance in the neural network. An MLP Classifier from Scikit-learn was used to model the EPNN, and prediction probabilities were output for each test sample. Best suitable server and all the parameters matched, we transfer the load to the respective server. For verification of the EPNN-based load balancing, we used the Event B platform with the Rodin tool. The tool generates the proof tree and proof obligation. Once the proof obligation is discharged and all the nodes in the proof tree are resolved, the proof obligation will be marked as proved. For validation, we implement a model in Python that calculates each server’s criteria and predicts the server status and its probability. First, we data processing, feature selection, model training, and testing the prediction. This setup calculates each row’s prediction individually and provides the server’s name and probability score. The key advantage of EPNN in load balancing is fast training, probability decision, and real-time load balancing, which is crucial for dynamic load balancing in cloud environments where request arrivals are frequent. Once the EPNN model is trained using server performance data (network traffic, server load, priority levels). It can be tested on new data to evaluate its performance. 7. Result For validation of the algorithm, Fig18 represents the predictions and probabilities for a test dataset in a load-balancing scenario using a machine learning model. A total of 40 samples were generated with server prediction and probabilities. Here is a breakdown of its contents: 1 . Sample X : Each row corresponds to an individual test sample. 2. Predicted Server : The predicted server that the model has selected for each test sample. The servers are labeled as s1, s2, s3, etc., up to s7. 3. Probabilities : This represents the probability distribution over all possible servers (s1 to s7) for each in EPNN, random forest, and logistic regression test samples. The values in the probability array are percentages that sum to 100, showing how confident the model is about selecting a sample server. This result shows that the EPNN model is more efficient as compared to the random forest and logistic regression. EPNN was more accurate, making it better suited for predicting server assignments in complex load-balancing scenarios. EPNN offered more refined probability distributions, providing a clearer picture of the confidence in its predictions. This makes it especially useful when decisions are based on probabilistic reasoning. The EPNN model was better at capturing intricate patterns in the data, thanks to its deep learning architecture. In contrast, random forest and logistic regression struggled to handle more complex, non-linear relationships. Classification Report of the EPNN model: Classification Parameter Precision Recall F1-score Support Class 0 (Low Priority) 0.56 0.67 0.61 128 Class 1 (High Priority) 0.57 0.46 0.51 123 Accuracy - - 0.56 251 Macro Avg 0.57 0.56 0.56 251 Weighted Avg 0.57 0.57 0.56 251 Table 1: Classification report of the EPNN model . The model's overall accuracy was 56%, indicating moderate performance in distinguishing between low-priority and high-priority requests. The precision for Class 1 (High Priority) was 0.57, meaning 57% of the instances predicted as high priority were correct. However, the recall for Class 1 was lower (0.46), indicating that the model missed 54% of actual high-priority cases. The macro average F1-score (0.56) suggests that the model maintains a relatively balanced performance across both classes, but there is room for improvement in recall. The weighted average F1-score (0.56) confirms that the model performs similarly across different class distributions. (See Table1) AUC-ROC Analysis To further evaluate the model’s discriminative ability, the AUC-ROC score was computed. The model achieved an AUC-ROC score of 0.56, indicating slightly better-than-random classification performance. To verify the algorithm, we implement an effective probabilistic neural network (EPNN) model in the Rodin tool. This model predicts server assignments for incoming requests. EPNNs are structured as neural networks, typically consisting of input, hidden, and output layers. The input layer receives features related to server load, threshold time, predefined time, deadline time, and request size. The hidden layer processes through interconnect nodes, and finally, the output layer generates a prediction of the optimal server assignment based on the learned patterns. After designing the model of EPNN load balancing, we implemented the events into the Event B tool on the RODIN platform for verification. All the events in the system are verified and validated with the Event B model. This model generates the proof obligations methods, which are manually or automatically discharged. Rodin tool generates a total of 122 proof obligations, 90 of which are discharged automatically, and 32 of which require manual interaction. (See Table 2) Element name Total P.O. Automatic P.O. Reviewed Discharged Context 0 0 0 0 Machine 112 90 22 0 Table 2: Proof obligations generated by the Rodin tool In model training and testing, despite Random Forest being faster and easier to train, EPNN proved to be more efficient in scenarios that require deeper insights and more precise predictions. For tasks such as server load balancing, where decisions can be critical and misclassifications costly, EPNN provides a better solution. EPNN finds the probability of transferring the load nearly 90%, while the Random Forest algorithm finds the correct server less than 40%. So, the difference is clear, the probabilistic neural network is more accurate and efficient for transferring the large dynamic load in cloud servers. The proposed EPNN-based load balancing algorithm advances the state of the art by addressing key challenges in dynamic and large-scale cloud environments. Unlike traditional load balancing solutions, which often rely on static rules or heuristics, the EPNN approach leverages probabilistic neural networks (PNNs) for advanced prediction capabilities. This enables the system to anticipate server load trends and proactively redistribute requests, reducing response times and preventing overload scenarios. The integration of probabilistic models provides robust decision-making under uncertainty. The critical enhancement is in environments with unpredictable workload patterns. 8. Conclusion This research proposes a forward-looking approach to load balancing in cloud computing by integrating Effective Probabilistic Neural Networks (EPNN) with formal modeling techniques such as Event-B. In cloud environments, data is growing day by day. We have proposed a methodology that aims to meet future demands by leveraging machine learning-driven mechanisms, including probabilistic matchmaking and intelligent data discovery, to dynamically and efficiently distribute workloads. The use of formal verification through the Event-B method and the Rodin tool ensures that the system remains logically sound and robust, even under rapidly changing conditions, thereby paving the way for high-reliability cloud infrastructures. Looking ahead, the incorporation of algorithms such as the Round Robin Assigning Algorithm (RRAA), Data Discovery Algorithm (DDA), and External Resource Access Algorithm (ERAA) positions the model to adapt seamlessly to future challenges like resource heterogeneity, increased demand, and real-time responsiveness. This makes the proposed solution not only scalable and efficient but also future-ready for evolving cloud computing ecosystems. This research bridges the gap between theoretical modeling and practical application by addressing real-world challenges in cloud-based load balancing. The proposed EPNN algorithm, verified through formal modeling, adapts dynamically to server conditions, making it suitable for commercial cloud environments like AWS, Microsoft Azure or private cloud. By optimizing resource usage and reducing processing delays, the model enhances user experience and lowers operational costs, offering a scalable and energy-efficient solution for next-generation data centers. In real-world deployment scenarios, the proposed approach can significantly reduce task response time, avoid server overloads, and optimize resource utilization, leading to improved quality of service (QoS) and enhanced user satisfaction. Declarations Acknowledgments: The author extends their gratitude to the Rajkiya Engineering College, Banda for their invaluable continuous support for this research work. Author contributions: Shantanu Shukla (Corresponding Author): conceptualization, data curation, investigation, methodology, formal analysis, writing—original draft. Vibhash Yadav: reviewing and editing. Corresponding author: Correspondence toShantanu Shukla Ethics Declarations Funding Declaration: No funding Ethics and Consent to Participate declarations: Not applicable Data Availability: The datasets generated and analysed during the current study are available in the https://www.kaggle.com/datasets/shantanushukla2207/load-balancing-dataset Consent to Publish declaration: not applicable Competing Interest declaration: The authors declare no competing interests References Ali.F & Khan.R, “The study on load balancing strategies in distributed computing system”, IJCSES, vol.3 no.2, page no. 19-30, 2012, DOI: 10.5121/ijcses.2012.3203 Anna. Hac, “Load balancing in distributed systems: A survey” , AT & T bell laboratories, Performance Evaluation Review, Vol. 16 dated on 2-4 February 1989 Othman.O & Douglas.C., “Optimizing distributed system performance via adaptive middleware load balancing”, University of California, April 2001 Tyagi.V & Tarun kr., “ORT Broker Policy: Reduce Cost and Response Time Using Throttled Load Balancing Algorithm”, Procedia Computer Science, Volume 48, 2015, Pages 217-221 D. A. Shafiq, N. Jhanjhi, and A. Abdullah, “Proposing A Load Balancing Algorithm for the Optimization of Cloud Computing Applications,” MACS 2019 - 13th Int. Conf. Math. Actuar. Sci. Comput. Sci. Stat. Proc., 2019, doi: 10.1109/MACS48846.2019.9024785. Violetta N. Volkova et.al. “Load balancing in cloud computing”, 2018 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus), Jan 2018, IEEE, DOI: 10.1109/EIConRus.2018.8317113 Caterina urban and Antoine Mine, “A review of formal methods applied to machine learning”, arXiv:2104.02466v2 [cs.PL] 21 Apr 2021 Emre Gures et.al. “Machine Learning-Based Load Balancing Algorithms in Future Heterogeneous Networks: A Survey” IEEE Access Vol 10, Page 37689-37717, DOI: 10.1109/ACCESS.2022.3161511 R. Agrawal, D.K. Sharma et.al. “Machine learning and deep learning based load balancing algorithms techniques in cloud computing”, 2021 International Conference on Innovative Practices in Technology and Management (ICIPTM), IEEE, April 2021, DOI: 10.1109/ICIPTM52218.2021.9388349 X. Hou and G. Zhao, \"Resource Scheduling and Load Balancing Fusion Algorithm with Deep Learning Based on Cloud Computing\", International Journal of Information Technology and Web Engineering (IJITWE), vol. 13, no. 3, pp. 54-72, 2018. C. Gomez, A. Shami and X. Wang, \"Machine Learning Aided Scheme for Load Balancing in Dense IoT Networks\", Sensors, vol. 18, no. 11, pp. 3779, 2018. S. Parida and B. Panchal, \"An efficient dynamic load balancing algorithm using machine learning technique in cloud environment\", International journal of scientific research in science engineering and technology, vol. 4, pp. 1184-1186, 2018. S. Moreno-Alvarez, J. M. Haut, M. E. Paoletti, J. A. Rico-Gallego, J. C. Diaz-Martin and J. Plaza, \"Training deep neural networks: a static load balancing approach\", The Journal of Super computing, vol. 76, no. 12, pp. 9739-9754, 2020. Thai Son Hoang, Jean Raymond Abrial “Event-B Patterns and Their Tool Support”, Software and Systems Modelling, May 2013, Vol 12 , issue 2, pp 229-244 Butler, Michael, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. \"The first twenty-five years of industrial use of the B-method.\" In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209. Springer, Cham, 2020. Butler, Michael. \"Decomposition structures for Event-B.\" In International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009. Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. \"Rodin: an open toolset for modelling and reasoning in Event-B.\" International journal on software tools for technology transfer 12, no. 6 (2010): 447-466. Nada M. Al Sallami et.al. “Load balancing with Neural Network”, The science and Information Organization, Volume 4 Issue 10, 2013, DOI: 10.14569/IJACSA.2013.041021 Sergio Moreno‑Álvarez et.al. “Training deep neural networks: a static load balancing approach” The journal of supercomputing, Springer Nature 2020, https://doi.org/10.1007/s11227-020-03200-6 Madhukar Prashant Shukla, Poonam Keswani, and Bright Keswani, “Artificial neural network based load balancing scheme for top of rack switches in optical data centers” Journal of Optical Communications, Published online by De Gruyter August 3, 2023, https://doi.org/10.1515/joc-2023-0189 Waldemar pokuta, Krzysztof Zatwarnicki, “Application of Neural Networks in Distribution of the Load in Cluster-Based Web Systems” Web Infrastructure Enhancement and Performance Evaluation, Appl. Sci. 2022, 12(1), 79; https://doi.org/10.3390/app12010079 Shantanu shukla, Raghuraj singh, Divakar Yadav, “Formal Modelling of Cluster-Coordinator-Based Load Balancing Protocol Using Event-B”, Proceedings of Second Doctoral Symposium on Computational Intelligence, pp-593-603, vol: 1374, Singapore. https://doi.org/10.1007/978-981-16-3346-1_48 Pooja Yadav, Raghuraj Suryavanshi, Divakar Yadav, “Formal Verification of Receiver Initiated Load Distribution Protocol with Fault Tolerance and Recovery using Event-B”, Journal of Scientific and Industrial Research (JSIR), Vol:80 issue: 12, April 2022, pp:1078-1090 Behshad Mohebali et. Al., “Probabilistic neural networks: a brief overview of theory, implementation, and application, Handbook of Probabilistic Models. https://doi.org/10.1016/B978-0-12-816514-0.00014-X, year- 2012 Fatma M. Talaat, Ahmed Ibrahim Saleh, Hesham Arafat Ali, “Effective Load Balancing Strategy (ELBS) for Real-Time Fog Computing Environment Using Fuzzy and Probabilistic Neural Networks, Journal of Network and Systems Management · October 2019, https://www.researchgate.net/publication/330916938 Resat Umit Payli, Kayhan Erciyes, Orhan Dagdeviren, “Cluster based load balancing algorithms for grids”, International Journal of Computer Networks & Communications (IJCNC) Vol.3, No.5, Sep 2011 Prabhdeep Singh et.al., “A fog based cluster based load balancing”, S ustainability 14, no. 13: 7961. https://doi.org/10.3390/su14137961 AnnaVictoria C R Oikawa, Vinicius Freitas, Márcio C Castro, Laércio Lima Pilla, “Adaptive Load Balancing based on Machine Learning for Iterative Parallel Applications”, Submitted on 12 May 2020, https://hal.science/hal-02570549 Chen, Shenghui & Fan, Zhiming & Shen, Haiying & Feng, Lu. (2019). Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods. 146-151. 10.1109/MASSW.2019.00036. S. Chen, Z. Fan, H. Shen and L. Feng, \"Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods,\" 2019 IEEE 16th International Conference on Mobile Ad Hoc and Sensor Systems Workshops (MASSW) , Monterey, CA, USA, 2019, pp. 146-151, doi: 10.1109/MASSW.2019.00036 Edwin ablad, “Mathematical modelling and methods for load balancing and coordination of multi robot stations”, Sweden 2022 Kai Zhang, Wei Guo, Jian Feng, “Load Forecasting Method Based on Improved Deep Learning in Cloud Computing Environment”, Scientific Programming Towards a Smart World: Hindawi Publication, Volume 2021, https://doi.org/10.1155/2021/3250732 E. Gures, I. Shayea, M. Ergen, M. H. Azmi and A. A. El-Saleh, \"Machine Learning-Based Load Balancing Algorithms in Future Heterogeneous Networks: A Survey,\" in IEEE Access, vol. 10, pp. 37689-37717, 2022, doi: 10.1109/ACCESS.2022.3161511. MUHAMMAD ASIM SHAHID, NOMAN ISLAM et.al., “A Comprehensive Study of Load Balancing Approaches in the Cloud Computing Environment and a Novel Fault Tolerance Approach” IEEE Access, Accepted by 4 July, 2020, Digital Object Identifier 10.1109/ACCESS.2020.3009184 M. Talaat, Fatma & Ali, Hesham & Saraya, Mohamed & Saleh, Ahmed. (2022). Effective scheduling algorithm for load balancing in fog environment using CNN and MPSO. Knowledge and Information Systems. 64. 1-25. 10.1007/s10115-021-01649-2. Malavika, R. & Valarmathi, M.. (2022). Adaptive Server Load Balancing in SDN Using PID Neural Network Controller. Computer Systems Science and Engineering. 42. 229-243. 10.32604/csse.2022.020947. Kaur, Amanpreet & Kaur, Bikrampal & Singh, Parminder & Devgan, Mandeep & Toor, Harpreet. (2020). Load Balancing Optimization Based on Deep Learning Approach in Cloud Environment. International Journal of Information Technology and Computer Science. 12. 8-18. 10.5815/ijitcs.2020.03.02. Yao, Zhiyuan & Desmouceaux, Yoann & Townsley, William & Clausen, Thomas Heide. (2021). Towards Intelligent Load Balancing in Data Centers. https://doi.org/10.48550/arXiv.2110.15788 L. Xu, H. H. Hoos, and K. Leyton-Brown. Hierarchical hardness models for SAT. In Conference on Principles and Practice of Constraint Programming, 2007 L. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown. Satzilla: Portfolio-based algorithm selection for sat. JAIR, 32:565–606, 2008 S. Tetsuya, A. Alejandra, B. Gilles et. Al, “Formal Verification of Higher-order probabilistic programming” (Reasoning about approximation), arxiv: 1807.06091V3[cs. L0] 25 Feb 2020 Poppleton, M. (2008). The Composition of Event-B Models. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_17 Abrial, JR., Butler, M., Hallerstede, S. et al. Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer 12, 447–466 (2010). https://doi.org/10.1007/s10009-010-0145-y Donald F. Specht, “Probabilistic neural networks”, Neural Networks, Volume 3, Issue 1, 1990, Pages 109-118, ISSN 0893-6080, https://doi.org/10.1016/0893-6080(90)90049-Q. Additional Declarations No competing interests reported. Cite Share Download PDF Status: Published Journal Publication published 15 Oct, 2025 Read the published version in Discover Computing → Version 1 posted Editor assigned by journal 20 May, 2025 Editorial decision: Revision requested 20 May, 2025 Reviews received at journal 13 May, 2025 Reviews received at journal 22 Apr, 2025 Reviewers agreed at journal 22 Apr, 2025 Reviewers agreed at journal 22 Apr, 2025 Reviewers invited by journal 22 Apr, 2025 Submission checks completed at journal 22 Apr, 2025 First submitted to journal 20 Apr, 2025 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {\"props\":{\"pageProps\":{\"initialData\":{\"identity\":\"rs-6006596\",\"acceptedTermsAndConditions\":true,\"allowDirectSubmit\":false,\"archivedVersions\":[],\"articleType\":\"Research Article\",\"associatedPublications\":[],\"authors\":[{\"id\":446314123,\"identity\":\"7ff2b772-3f4e-4cc2-a963-896ee5bb17c0\",\"order_by\":0,\"name\":\"Shantanu Shukla\",\"email\":\"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAABHUlEQVRIie3PPUvEMBjA8chBbwl0fUTtfYVIoDr4YfJw0FtykyAORQ4KnaRz4IR+hUKhcyVYF90DdhCFmw+Ejj1b5EChFdwc8h9CAvnlhRCb7R82U/sZkAl5JRfUha/l8RhhphvKPREk8A4VOVh1SzpK4CfRvDukJ2ScHEWb921YY7q+5UyEE8xfosc3E55TMtUP2dBf7qozVlYbzOonLkTlYFFXGMmqexgNAjN0jRE+lI7GDCQvhUOxMPI0kk5HgPrDZNFA2WpMVU9awFz1pP2NSB/uY40rI7nAmHEGHVnG44QZeQXPieaZCS4ZJsIDE+B6mQB1Rv4yU4sCrht9kqp5DttmR101Lz9kc+O5U10NPmw852/bbTabzfatTybRbWCmtkjSAAAAAElFTkSuQmCC\",\"orcid\":\"\",\"institution\":\"Rajkiya Engineering college, Banda\",\"correspondingAuthor\":true,\"prefix\":\"\",\"firstName\":\"Shantanu\",\"middleName\":\"\",\"lastName\":\"Shukla\",\"suffix\":\"\"},{\"id\":446314124,\"identity\":\"5ae5adfa-ca3d-4b82-b488-b7a478fc9015\",\"order_by\":1,\"name\":\"Vibhash Yadav\",\"email\":\"\",\"orcid\":\"\",\"institution\":\"Rajkiya Engineering college, Banda\",\"correspondingAuthor\":false,\"prefix\":\"\",\"firstName\":\"Vibhash\",\"middleName\":\"\",\"lastName\":\"Yadav\",\"suffix\":\"\"}],\"badges\":[],\"createdAt\":\"2025-02-11 10:53:27\",\"currentVersionCode\":1,\"declarations\":\"\",\"doi\":\"10.21203/rs.3.rs-6006596/v1\",\"doiUrl\":\"https://doi.org/10.21203/rs.3.rs-6006596/v1\",\"draftVersion\":[],\"editorialEvents\":[{\"content\":\"https://doi.org/10.1007/s10791-025-09748-2\",\"type\":\"published\",\"date\":\"2025-10-15T15:58:15+00:00\"}],\"editorialNote\":\"\",\"failedWorkflow\":false,\"files\":[{\"id\":81248942,\"identity\":\"a677f9a6-36c7-4eba-82d1-7d0a77673246\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:42\",\"extension\":\"jpg\",\"order_by\":1,\"title\":\"Figure 1\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":58202,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eFlow chart of EPNN-based Load Balancing in Cloud Environment\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"1.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/f566f0979031a6c6cb18da36.jpg\"},{\"id\":81249757,\"identity\":\"620366b5-792f-488f-be63-6adab238922b\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:43\",\"extension\":\"jpg\",\"order_by\":2,\"title\":\"Figure 2\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":108447,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eInvariants of the EPNN-based algorithm\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"2.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/40117d1d3e90e2d2d6920f94.jpg\"},{\"id\":81249753,\"identity\":\"59b64345-42f4-4664-b393-b77e62e7d68a\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:42\",\"extension\":\"jpg\",\"order_by\":3,\"title\":\"Figure 3\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":22285,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eCreate Cluster Group\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"3.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/02679896f45170bede1d2a3d.jpg\"},{\"id\":81248944,\"identity\":\"c9c5f574-eecb-46bb-a460-66e9184d1cc5\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:42\",\"extension\":\"jpg\",\"order_by\":4,\"title\":\"Figure 4\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":41068,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eSending the new req. into cluster\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"4.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/a3ac301091f12de7a30480af.jpg\"},{\"id\":81250160,\"identity\":\"775ac7b4-c560-4430-bfca-5cf52ec0849f\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 03:06:42\",\"extension\":\"jpg\",\"order_by\":5,\"title\":\"Figure 5\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":28690,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eDeclare the coordinator in cluster\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"5.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/e3facb685ad11916084cab22.jpg\"},{\"id\":81248950,\"identity\":\"66cfd92a-d2d6-4514-85bd-074712cf082d\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":6,\"title\":\"Figure 6\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":66738,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eDelivery of Request message\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"6.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/7f305010e0a1ef2acf583f03.jpg\"},{\"id\":81249756,\"identity\":\"3c859a27-e33d-47d1-8868-451c63c2753a\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:42\",\"extension\":\"jpg\",\"order_by\":7,\"title\":\"Figure 7\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":69302,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eThe Nearest Cloud will be chosen\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"7.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/4f83d9a67ab9df07643d600f.jpg\"},{\"id\":81249754,\"identity\":\"a9550a2c-4438-486a-bbd0-c54e5f72dfb5\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:42\",\"extension\":\"jpg\",\"order_by\":8,\"title\":\"Figure 8\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":30926,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eIf request is already predefined request\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"8.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/9e7fb6b2472f662bfec5d9ba.jpg\"},{\"id\":81248954,\"identity\":\"b032a95a-5c8d-4163-a61c-bf659d624e59\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":9,\"title\":\"Figure 9\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":52075,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eSend the reply into node from the server \\u0026nbsp;manager\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"9.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/4ebc7870344053a31e5a0cba.jpg\"},{\"id\":81249758,\"identity\":\"3aa5cb0a-a612-4cce-8bc3-3c8e3440dce1\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:43\",\"extension\":\"jpg\",\"order_by\":10,\"title\":\"Figure 10\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":55320,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eIf the request is not found in the server manager\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"10.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/32dd23b6979e68332955815a.jpg\"},{\"id\":81248958,\"identity\":\"c1d40fb5-73c9-4eaa-ba28-2f99afec6f49\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":11,\"title\":\"Figure 11\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":63122,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eIf the required capability is not matched in the server\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"11.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/367aa2de14bdcbd777964bfb.jpg\"},{\"id\":81248971,\"identity\":\"cf096909-3dc8-4fa6-8705-e1993c4aea45\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":12,\"title\":\"Figure 12\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":58077,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eChoose another appropriate cluster\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"12.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/08c3c480efa3139d9b6c4509.jpg\"},{\"id\":81248956,\"identity\":\"85d127dd-20c4-4870-b9e0-ea837ea6ebe6\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":13,\"title\":\"Figure 13\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":29081,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eChoosing the best server using Round robin techniques\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"13.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/c48850aacd4165785ea43f59.jpg\"},{\"id\":81249762,\"identity\":\"80cd71a2-7af3-4f34-8cc8-953e3280fbc0\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:43\",\"extension\":\"jpg\",\"order_by\":14,\"title\":\"Figure 14\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":31381,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eEPNN algorithm for selecting the best node\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"14.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/8736ba3df71614e11d4d77c5.jpg\"},{\"id\":81248961,\"identity\":\"4916c469-3481-4ef5-9ad4-5f57f48e8e30\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:43\",\"extension\":\"jpg\",\"order_by\":15,\"title\":\"Figure 15\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":29319,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eEPNN matchmaking algorithm\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"15.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/61447e4e27e4e0ff27c87360.jpg\"},{\"id\":81250843,\"identity\":\"90ee15a7-b79d-4c7f-9e95-d4bb812b6ad2\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 03:14:44\",\"extension\":\"jpg\",\"order_by\":16,\"title\":\"Figure 16\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":74264,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eIf new request is not processed in the same server\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"16.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/ee2b9123c54370aec5088a98.jpg\"},{\"id\":81249765,\"identity\":\"81aa5472-5871-4984-9b66-16956cde342b\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:58:43\",\"extension\":\"jpg\",\"order_by\":17,\"title\":\"Figure 17\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":43328,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eMake a PNN coordinator\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"17.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/a0acc8a04e4a8cbfdaa360ad.jpg\"},{\"id\":81248980,\"identity\":\"424873f4-fcf2-43bb-903f-313f90c96ba6\",\"added_by\":\"auto\",\"created_at\":\"2025-04-24 02:50:44\",\"extension\":\"jpg\",\"order_by\":18,\"title\":\"Figure 18\",\"display\":\"\",\"copyAsset\":false,\"role\":\"figure\",\"size\":92074,\"visible\":true,\"origin\":\"\",\"legend\":\"\\u003cp\\u003e\\u003cstrong\\u003eResults of Prediction and probabilities of 7 test samples for EPNN, Random Forest and logistic regression for the same dataset and graphical representation\\u003c/strong\\u003e\\u003c/p\\u003e\",\"description\":\"\",\"filename\":\"18.jpg\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/44c78e67e9aee2840d42b4a4.jpg\"},{\"id\":93956044,\"identity\":\"7a933edf-e69a-4330-91e9-a673bc33766a\",\"added_by\":\"auto\",\"created_at\":\"2025-10-20 16:09:43\",\"extension\":\"pdf\",\"order_by\":0,\"title\":\"\",\"display\":\"\",\"copyAsset\":false,\"role\":\"manuscript-pdf\",\"size\":3242460,\"visible\":true,\"origin\":\"\",\"legend\":\"\",\"description\":\"\",\"filename\":\"manuscript.pdf\",\"url\":\"https://assets-eu.researchsquare.com/files/rs-6006596/v1/dec63bb7-504c-4e7b-8749-8fdb4e47d7bb.pdf\"}],\"financialInterests\":\"No competing interests reported.\",\"formattedTitle\":\"Formal Modelling and Verification of Effective Probabilistic Neural Networks for Load Balancing in a Cloud Environment\",\"fulltext\":[{\"header\":\"1. Introduction\",\"content\":\"\\u003cp\\u003e\\u003cstrong\\u003e1.1 General Perspective\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eLoad balancing is an important concept in distributed and cloud computing fields where the data is involved and accessed for efficient distribution of workloads or network traffic across multiple resources to ensure optimal resource utilization, maximize performance, and minimize response time\\u0026nbsp;[1] [2]. Load balancing is a comprehensive and essential strategy for efficiently distributing tasks, requests, or data across multiple servers, clusters, resources, or network links. Its primary goal is to prevent any single resource from becoming overloaded. By evenly distributing the workload, load balancing ensures optimal utilization of resources, resulting in enhanced system performance, greater scalability, and improved overall network reliability [3]. Different type of key concepts ensures load distribution, like resource utilization, where a loaded task or request receives the load and an overloaded task sends the load to maximize resource utilization\\u0026nbsp;[4]. Another fundamental concept in load balancing is fault tolerance, which ensures system reliability by rerouting requests or tasks away from failed or underperforming resources. Additionally, performance improvement plays a vital role, as effective load balancing significantly reduces response times and enhances the overall efficiency and responsiveness of the system. Different load balancing algorithms [5] determine how to distribute the traffic or tasks, like round robin, least connection, weighted round robin, sender-initiated, receiver-initiated, and many more. The balancing approach in cloud computing is an important concept because managing the load and providing services to every client is essential. Cloud computing is an essential concept in the computer science field where the cloud refers to the internet or network. It is a technology where all the tools are accessed remotely and store, manage, and access the data online rather than locally\\u0026nbsp;[6].\\u003c/p\\u003e\\n\\u003cp\\u003eNumerous studies have been presented concerning machine learning with load balancing [7]\\u0026nbsp;[8]. Load balancing in machine learning refers to the practice of addressing imbalanced datasets or uneven class distributions to ensure that machine learning models perform effectively and make fair predictions. There are different methodologies like resampling techniques\\u0026nbsp;[9], ensemble methods, anomaly detection deep learning methods, etc\\u0026nbsp;[10]. The choice of load balancing technique depends on the nature of the problem, the availability of data, and the desired performance metrics. It's essential to experiment with different approaches and evaluate their impact on your specific machine-learning problem to find the most effective solution. However, there are a few papers \\u0026nbsp;[11] available to introduce the load balancing models in machine learning and neural networks\\u0026nbsp;[12] [13]. Our research work is divided into 2 types, The first part introduces how to create an effective probabilistic neural network model of load balancing [14] [15] and the second part introduces how the model will you verified and validated with the Event-B tool [16] [17]. Both parts of our research work are introduced in this paper.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003eIn this paper, we introduced the concept of round robin assigning algorithm (RRAA) for newly arrived requests, a data discovery algorithm (DDA) for finding the perfect node or cluster, effective probabilistic neural network (EPNN) for distribution of the load in the best cluster. The EPNN algorithm helps to choose the best coordinator and perform the load distribution algorithm [18] [19] in the neural network environment [20] [21]. Formal modelling [22] [23]of the EPNN algorithm [24] is necessary for checking the correctness and mathematical proof of the algorithm. Depending upon the context and machine part of the algorithm, the proof obligation is constructed by the machine and generates the proof trees and methods to identify the working of the algorithm is working correctly. [25] These proof generation 2 types, the first one is automated, and the second one is done manually. If the event is not correctly associated with invariants or context parts, make them correct manually. This work differs from existing\\u0026nbsp;traditional approaches, our method combines Effective Probabilistic Neural Networks (EPNN) with formal verification using Event-B to ensure both predictive adaptability and system correctness in cloud load balancing.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1.2 Problem Statement\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eIn cloud computing environments, efficient load balancing is critical to ensure optimal resource utilization, minimized response time, and reliable load transfer between the nodes. Traditional load balancing techniques often struggle to dynamically adapt to varying workloads and unpredictable system behaviours, leading to performance bottlenecks, underutilization, or overload of computational nodes. Moreover, these algorithms lack formal verification, making it difficult to guarantee correctness and reliability in real-time cloud systems.\\u003c/p\\u003e\\n\\u003cp\\u003eThis research paper addresses these limitations by proposing a formally verified Enhanced Probabilistic Neural Network (EPNN) based load balancing algorithm. The problem lies in designing a load balancing solution that not only adapts to real-time fluctuations using intelligent prediction models but also ensures correctness and fault tolerance through formal methods. The proposed work aims to model, implement, and formally verify the EPNN approach using Event-B and the Rodin tool, ensuring both high performance and provable reliability in dynamic cloud environments.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1.3 Research Motivation\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eCloud computing offers scalability, flexibility, and on-demand access to computational resources. However one of the determining challenges in the cloud environment is efficient load balancing, which ensures that the load of the servers is evenly distributed across the servers to maintain performance and optimize resource usage. A traditional load balancing algorithm that adapts to rapid workload fluctuations and uncertain resource availability. Recent advancements in machine learning, particularly Probabilistic Neural Networks (PNNs), offer promising capabilities for predicting and managing dynamic workloads through intelligent decision-making. Yet, despite their predictive power, such models are rarely integrated with formal methods that can ensure correctness, consistency, and reliability. By developing an enhanced PNN-based load balancing algorithm and formally modeling it using Event-B in the Rodin platform, this work aims to deliver a solution that is not only intelligent and adaptive but also mathematically verified for correctness.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1.4 Organization of Paper\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eThe organization of the paper is as follows: Section 2 introduces the background of the load balancing algorithm, effective probabilistic neural network, and formal modelling. Section 3 briefly outlines the related work. Section 4 described the working of the proposed effective load balancing algorithm with an effective probabilistic neural network algorithm. Section 5 presents the Event-B model of EPNN-based load balancing. Section 6 presents EPNN Load Balancing validation with Metrics. Section 7 characterizes the result analysis of the proposed model, and Section 8 concludes the paper.\\u003c/p\\u003e\"},{\"header\":\"2. Background\",\"content\":\"\\u003cp\\u003eThis section presents several key concepts related to the domain of cloud computing., request scheduling, load balancing, effective probabilistic neural networks (EPNN), formal modelling, and neural network algorithms.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eA. Cloud computing:\\u0026nbsp;\\u003c/strong\\u003eCloud Computing is the popular and on-demand availability of different types of resources related to the computer system, like virtual systems, including file networks, memory areas, and databases. Cloud Computing operates with a service model that is divided into 4 layers. The top layer shows cloud clients such as web browsers, IOT, and digital computing devices, and the second layer communicates with the software as a service (SAAS), such as email, virtual desktop, group chat, etc. The third layer provides the platform as a service (PAAS), programming languages, libraries, application runtime database et.al. \\u0026nbsp;The fourth layer offers Infrastructure as a Service (IaaS), providing access to virtual machines, load balancers, networks, and storage. This layer forms the foundation of cloud-based resources. The bottom layer of the cloud computing model is the deployment model, which includes various types of cloud environments such as hybrid cloud, multi-cloud, and public cloud.\\u003c/p\\u003e\\n\\u003cp\\u003eA large cloud provides the functionality of distributed resources over multiple servers, each of which is called a data center. Cloud Computing shares the sources and performs the work pay-as-you-go model, which reduces the burden of monthly expenses. The main advantages of cloud computing are reduction, device independence, a large set of storage, expanded availability, increased productivity, and security measures.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eB. Request scheduling algorithm:\\u003c/strong\\u003e The request scheduling algorithm plays an important role in cloud systems. The request algorithm ensures the efficient utilization of resources, load balancing, and timely replies from servers to user requests. In this section, different types of scheduling algorithms are used in cloud systems.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1. Round Robin (RR) algorithm:\\u003c/strong\\u003e This is a simple and widely used algorithm. Requests are assigned cyclically, so there are no deadlocks and starvation conditions arise. Each server gets an equal opportunity to balance the load. The advantage of the RR algorithm is that it is easy to implement and understand, but the disadvantage of this algorithm is that it does not calculate the server load or request complexity.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e2. Weighted Round Robin scheduling:\\u003c/strong\\u003e Like Round Robin, servers are assigned different weights based on their capacity or processing power. Servers with higher weights get more requests. The advantage of this algorithm is that more important requests are served first, and then all other requests are served based on their weights. The disadvantage of this algorithm may not be optimal for heterogeneous server capacities.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e3. Least connection Scheduling:\\u0026nbsp;\\u003c/strong\\u003eRequests are assigned to those servers that are least loaded during the transmission. Better resource utilization and maximum throughput are the main aims of this algorithm. The disadvantage of this algorithm is does not consider server performance on response time.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e4. Random Scheduling:\\u0026nbsp;\\u003c/strong\\u003eIn this algorithm, requests are assigned to random servers, which does not guarantee the optimal utilization of servers. The advantage of this algorithm is simplicity and uniform distribution of requests. Disadvantages of this algorithm lack of control and a lack of proper utilization of servers.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e5. Least response time scheduling:\\u0026nbsp;\\u003c/strong\\u003eAssign requests to the servers with the shortest response time. This algorithm mainly focuses on the reduced latency of the user. The disadvantage of this algorithm is the continuous monitoring of the response time.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e6. Priority Scheduling:\\u0026nbsp;\\u003c/strong\\u003eAssign priorities to the different types of users or requests. High-priority requests are processed before the low ones. The advantage of this algorithm is allowing for the prioritization of the critical tasks. The disadvantage of this is low low-priority tasks may lead to a starvation condition.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eC. Load balancing:\\u0026nbsp;\\u003c/strong\\u003eLoad balancing is a critical component in distributed systems, ensuring that resources are efficiently allocated and workloads are evenly distributed among servers or nodes. It aims to optimize performance, maximize resource utilization, and prevent system overloads. Here are the key aspects of load balancing in distributed systems:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1. Equal distribution of workload:\\u003c/strong\\u003e Load-balancing algorithms distribute incoming requests or tasks evenly across multiple servers or nodes. This prevents any single server from becoming overwhelmed while others are underutilized, leading to improved system efficiency.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e2.\\u003c/strong\\u003e \\u003cstrong\\u003eImproved Performance:\\u003c/strong\\u003e Evenly distributed workloads lead to improved system performance. When requests are distributed effectively, response times are reduced, and users experience faster service, which is crucial for web applications and services.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e3. Scalability:\\u003c/strong\\u003e Load balancing is essential for scaling a distributed system. As the system grows, you can add more servers or nodes and use load balancing to ensure that the new resources are used effectively.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e4. High Availability:\\u003c/strong\\u003e Load balancing also provides high availability. If one server fails, load balancers can automatically reroute traffic to healthy servers, reducing the risk of service interruptions.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e5. Dynamic Adaptation:\\u003c/strong\\u003e Some load balancers use machine learning and real-time data to make dynamic routing decisions. They adapt to changing traffic patterns and server conditions.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eD. Effective Probabilistic Neural Network:\\u0026nbsp;\\u003c/strong\\u003eProbabilistic Neural Networks (PNNs) are a class of neural network models that are particularly effective in various pattern recognition and classification tasks. They offer a probabilistic approach to decision-making, making them valuable for both classification and estimation problems. An \\u0026quot;Effective Probabilistic Neural Network\\u0026quot; (EPNN) in the context of load balancing is an innovative approach that integrates the principles of Probabilistic Neural Networks (PNNs) with additional features and adaptations to face the challenges posed by load balancing in cloud systems. EPNNs are designed to optimize the allocation of incoming requests to servers or nodes, ensuring efficient resource utilization and timely response to user requests.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eE. Formal Modelling:\\u003c/strong\\u003e Formal methods are techniques used to change the complex model into mathematical notation. A formal model provides a mathematical foundation for system-level modelling, verification, and validation. The advantage of formal methods is that they help ensure the correctness and safety of systems by enabling rigorous analysis of them properly. Formal modelling is particularly valuable for critical systems where safety and correctness are of utmost importance, as it allows for early detection of design flaws and verification of system behaviour against specified requirements. It provides a structured framework for system specification and verification that enhances the quality and dependability of software-based systems.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eF. Neural Network algorithm:\\u0026nbsp;\\u003c/strong\\u003eNeural networks have emerged as a powerful tool in the field of machine learning, drawing inspiration from the structure and functionality of the human brain. These networks consist of interconnected nodes, referred to as neurons, that are arranged in layers. Each neuron receives inputs, processes them, and passes the information through weighted connections to subsequent layers. The output generated from this process is determined by the weights and activation functions within the network, enabling neural networks to model complex patterns and relationships in data.\\u003c/p\\u003e\\n\\u003cp\\u003eInitially developed for tasks such as image recognition and natural language processing, neural networks have now found extensive application in a wide range of fields. Their ability to learn from data and generalize from examples makes them highly suitable for dynamic, real-time decision-making scenarios, including cloud computing, robotics, and financial modeling. In particular, deep learning, a subset of neural networks with multiple hidden layers, has significantly enhanced the capabilities of traditional machine learning algorithms, offering improved accuracy in prediction and classification tasks.\\u003c/p\\u003e\\n\\u003cp\\u003eThe flexibility of neural networks allows them to adapt to diverse datasets, handling non-linear relationships and high-dimensional data more efficiently than many classical algorithms. This adaptability is especially relevant in areas like load balancing and resource management in distributed systems, where complex interactions between numerous factors must be considered to optimize performance. In this context, neural networks serve as a robust framework for developing intelligent systems capable of handling the unpredictable and evolving nature of real-world environments.\\u003c/p\\u003e\"},{\"header\":\"3. Related Work\",\"content\":\"\\u003cp\\u003eInitially, this section introduces some previous work in the field of formal modelling with different machine learning techniques and real-time task scheduling. There are many existing works on the concept of neural networks. In a survey about load balancing with cluster coordinators using different machine learning technologies \\u0026nbsp;[26] [27] [28]. Formal modelling-based papers in load balancing also play an important role in my research [29] [30] [31]. In this paper, different methods of load forecasting on deep learning in cloud architecture are used. Different algorithms proposed by the author, such as the load forecasting process in Spark architecture and the data partition algorithm, explain the whole framework of the load forecasting and load classification. This paper\\u0026nbsp;[32] defines the load balancing strategy based on deep learning for multiple controllers in SDN to solve the load imbalance problem. The Q-values for switch migration actions are derived using a Double Deep Q-Network (DDQN), which is then trained through a replay mechanism to fine-tune and optimize the Q-network parameters. In [33] this survey paper, machine learning-based load balancing algorithm in the future heterogeneous network. This survey provides a guidelines and roadmap for developing the new load balancer models in future heterogeneous networks. Key performance indicator (KPI) used in the evaluation of load balancing models, along with load balancing the relationship between the concurrent optimization of coverage (CCO) and mobility robustness optimization (MRO). In [34] this paper is a comprehensive study of load-balancing approaches in cloud computing environments with fault-tolerant approaches. This paper also discusses the problem of load balancing in the cloud computing environment and identifies the need for a best load-balancing algorithm that combines fault tolerance metrics.\\u003c/p\\u003e\\n\\u003cp\\u003eNow, we have discussed some research papers that are based on neural networks, genetic algorithms, deep learning, CNN, MPSO, probabilistic neural networks, software-defined networks, and reinforcement learning. In this paper [35], the effective dynamic load balancing (EDLB) algorithms using CNN. After that, particle swarm optimization (PSO) is used for advanced modification, and results show that ELBS shows recent load balancing techniques to achieve the minimum average turnaround time (TAT) and fog resource monitor (FRM). This paper [36] presents the study of the application of adaptive load balancing implemented in ECDN servers. A neural network controller using a proportional-integral-derivative (PID) algorithm was developed to achieve near-optimal performance. In this paper [37], the author presents the significance of deep learning approaches that have been analyzed in the area of cloud computing using DLD-PLB. The paper presents the framework for workflow execution in a cloud environment that has been proposed and implemented with dynamic virtual machines and load balancing. In the paper [38] work connects the fields of machine learning and networking systems, showcasing how machine learning can be applied to network load balancers. It also highlights additional challenges that need to be addressed for the successful integration of machine learning into network systems.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp;Another field of research work implemented in this paper is formal modelling techniques implemented in load balancing and machine learning approaches. There are different papers implemented in this field. Most of the papers are implemented in different formal verification and validation themes under SAT-SMT, theorem proving, model checking, prediction, probabilistic programs, neural networks, and many other themes. In this paper [39], the author presents the hierarchical hardness model for Boolean satisfiability (SAT), which determines the satisfiability of a Boolean set of equations for a set of inputs. This paper is implemented under the classification task of machine learning. This paper [40] presents the widely observed fact that there is no single ‘dominant’ SAT solver. This methodology takes as input a distribution of problem instances and a set of solvers, then constructs a portfolio optimizing a given objective function. A decision tree-based machine learning algorithm is implemented in this paper. In this paper [41], probabilistic programming is used in reasoning about approximation, convergence, Bayesian inference, and optimization methods to prove with formal verification techniques. This work is based on a directed acyclic graph (DAG) machine learning task and a stochastic computation graph (SCG) based machine learning algorithm.\\u003c/p\\u003e\\n\\u003cp\\u003eAll these papers are present on formal verification and validation based on many research areas. We survey about two themes; the first survey is about the comparisons table between all ML/NN/DL oriented formal verification or validation and the second comparison is based on all ML/NN/DL oriented and load balancing algorithms.\\u003c/p\\u003e\"},{\"header\":\"4. Working of the Proposed effective Load balancing Algorithm with EPNN\",\"content\":\"\\u003cp\\u003eIn server management, load balancing plays an important role in optimizing resource utilization, maximizing throughput, and minimizing response time. It is an extremely significant issue to achieve load balancing among the cluster and its servers and nodes. Load balancing is a technique in server management to distribute the load between servers equally to increase performance, such as fail-over, and avoid bottlenecks and scalability. The load balancer strategy proposed in this paper with a help of neural network strategy. This strategy is based on an effective probabilistic matchmaking neural network algorithm. In this algorithm, we match the load for the best server. If the best server is found, it is completed. Otherwise, we send the request again to the server manager and choose another one. After choosing the best server, we select the new coordinator, called the probabilistic neural network coordinator.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp;The proposed architecture represents how the servers are allocated in the cloud environment and interconnected with each other. Each request can access its neighbour via wireless, and the request is saved in the dictionary, and the coordinator will choose to right server to process the load. The proposed architecture has been implemented to solve the issue related to execution time, throughput, and proper resource utilization. The EPNN-based algorithm performs the major role of sequencing, sending data, and receiving replies. This neural network algorithm used a string-matching algorithm for choosing the most efficient underloaded server. Each process has a few parameters that reflect the needed capabilities of the server, which are:\\u003c/p\\u003e\\n\\u003cp\\u003e1) CPU power needed for each server.\\u003c/p\\u003e\\n\\u003cp\\u003e2) Memory space needed for each server\\u003c/p\\u003e\\n\\u003cp\\u003e3) Storage requirement needed for the server, which reflects the needed cache size\\u003c/p\\u003e\\n\\u003cp\\u003e4) Each server needed the threshold value so that none of the servers crossed the threshold.\\u003c/p\\u003e\\n\\u003cp\\u003eThe cloud servers can distribute the requests equally. If all the capabilities match the parameters, then the load will be transferred accordingly. Choosing the EPNN load balancing algorithm helps to highlight its innovation and effectiveness. This neural network provides the advantages of dynamic adaptability, prediction-driven decision-making, energy efficiency, and threshold-based rules.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eProposed Algorithm\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eAlgorithm: EPNN-Based Load Balancing Strategy\\u003c/p\\u003e\\n\\u003cp\\u003e1. \\u0026nbsp;Initialize Cluster Groups: C1, C2, C3\\u003c/p\\u003e\\n\\u003cp\\u003e2. \\u0026nbsp;Receive New Request R1\\u003c/p\\u003e\\n\\u003cp\\u003e3. \\u0026nbsp;Select Nearest Cluster:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Chosen_Cluster ← NearestCluster(R1)\\u003c/p\\u003e\\n\\u003cp\\u003e4. \\u0026nbsp;Decide Cluster Coordinator for each cluster group\\u003c/p\\u003e\\n\\u003cp\\u003e5. \\u0026nbsp;IF R1\\u0026nbsp;∈\\u0026nbsp;PreRequestTable (PRT) THEN\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; ServerManager retrieves the required data from PRT\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Send data to Request R1\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; ELSE\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; ServerManager checks the required capabilities of R1\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; IF Capabilities_Match = TRUE THEN\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudServer executes R1\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Send a reply to the requester\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; ELSE\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudManagerServer (CMS) initiates Data Discovery Algorithm (DDA)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; IF Capabilities_Match = FALSE AND All_Servers_Overloaded THEN\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudMasterServer selects alternate cluster:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Use Round Robin (RR) to select a cluster with:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; - Highest Priority\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; - Most Underloaded Coordinator\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Use EPNN to search CloudMasterTable for the best-fit server\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; IF Suitable_Server_Found THEN\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Underloaded_Server replies and takes the load\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudManager assigns requests using RR based on capability\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Update Formal Model:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Set Server.Pattern_Match ← TRUE\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; ELSE\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Create New Node:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Designate as PNN Coordinator to coordinate the load\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Assign searching another intermediate cluster responsibility for the load\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e4.1 Description of EPNN, RRAA, DDA, Event-B and Rodin tool\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eIn this paper, we introduce the machine learning-based concepts regarding the effective probabilistic neural network (EPNN), external resource access algorithm (ERAA), round robin assigning algorithm (RRAA), and data discovery algorithm (DDA). These terms help the modelling with load balancing in a dynamic environment.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eA) Round robin Assigning Algorithm:\\u003c/strong\\u003e RR algorithm identified the cloud mastering server (CMS) for all the upcoming requests.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eInput:\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eA) Cloud Architecture\\u003c/p\\u003e\\n\\u003cp\\u003eB) Identified cloud master server (CMS)\\u003c/p\\u003e\\n\\u003cp\\u003eC) Master server manager (MSM)\\u003c/p\\u003e\\n\\u003cp\\u003eD) Initial value in round-robin assigning table (RRAT)\\u003c/p\\u003e\\n\\u003cp\\u003eE) Arrival time calculating server (ATCS)\\u003c/p\\u003e\\n\\u003cp\\u003eF) Arrived Request (RA)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eOutput:\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eArrival Time Assigning Table (ATAT)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eSteps of the RRA Algorithm:\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eFor each incoming request Ra:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; ServerManager → send Ra to TimeCalculatingServer (TCS)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; TCS:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Calculate NewArrivalTime (NAT) using fuzzy logic based on:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; - Predefined Time (PT)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; - Deadline Time (DT)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; - Request Size (RS)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Arrange all requests in ascending order of NAT\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; If multiple requests have the same NAT:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Sort those requests by Turnaround Time (TAT)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; End If\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Enqueue the sorted requests into PriorityQueue\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Send PriorityQueue to CloudMasterServer (CMS)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; CMS:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; For each request in PriorityQueue:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Try to serve the request on the selected optimal server\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; If request cannot be served:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; TCS → recalculate Turnaround Time (TAT)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Forward the request to another cluster\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; End If\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; End For\\u003c/p\\u003e\\n\\u003cp\\u003eEnd For\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eB) Data Discovery Algorithm:\\u0026nbsp;\\u003c/strong\\u003eFor each request, if the required data is not found in the local cloud cache, some steps will be performed:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1)\\u0026nbsp;\\u003c/strong\\u003eIf the required data is not available in the assigned cloud cache, the cloud master server will send the request to its neighbour using the data discovery algorithm (DDA).\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e2)\\u0026nbsp;\\u003c/strong\\u003eIf none of the master servers are sufficient to adjust the request, send it to another cloud master server (CMS) and send a cancel message to the other server’s node.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eSteps of the DDA Algorithm:\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eFor each incoming request Ra:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; If the data required for Ra is available in the cloud server's cache:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudServer → perform Ra\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; CloudServer → send reply to requester\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; Else:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; ServerManager → forward Ra to another CloudMasterServer (CMS) for processing\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; End If\\u003c/p\\u003e\\n\\u003cp\\u003eEnd For\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eC) External Resource Access Algorithm (ERAA):\\u0026nbsp;\\u003c/strong\\u003eIf the resource is not found in the master server, then search for the resource in another cloud.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eSteps of the ERA Algorithm\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eFor each requesting Cloud Master Server (CMS):\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; CMS → send data request to its neighbor CMS\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; For each receiving neighbor CMS:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; If the required data is found:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Neighbor CMS → send data to requesting CMS\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Else:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Neighbor CMS → reply with \\\"Not Found\\\" message\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; End If\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; End For\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; If data is not found in the neighbor CMS:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; Requesting CMS → send a request to another cloud to search for the resource\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; End If\\u003c/p\\u003e\\n\\u003cp\\u003eEnd For\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eD) Effective probabilistic neural network (EPNN)\\u0026nbsp;\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1) Input layer:\\u0026nbsp;\\u003c/strong\\u003eThe input layer consists of nodes representing various input features or parameters related to workload distribution.For example: CPU usage, Network traffic, memory usage\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e2) Pattern Layer:\\u0026nbsp;\\u003c/strong\\u003eThe pattern layer is responsible for storing the pattern and relationship between the input feature and the corresponding load distribution.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e3) Summation Layer:\\u0026nbsp;\\u003c/strong\\u003eWeighted summation of the output of the pattern layer.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e4) Output Layer:\\u0026nbsp;\\u003c/strong\\u003eThe output layer represents the load distribution across the available server. In this layer, the most suitable server will be chosen from all the servers after the processing in the summation layer.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; A matchmaking process using an Effective Probabilistic Matchmaking Neural Network (EPNN) algorithm. The goal of this process is to select the most appropriate server from a set of candidate servers based on certain conditions and then update the pattern-matching status. We will make a new PNN coordinator in place of the cluster coordinator to coordinate the load.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eE) Event B:\\u0026nbsp;\\u003c/strong\\u003eEvent B [42] is the formal method used in formalizing and developing systems for system-level specification design and verification. It provides a structured approach to modeling complex systems, aiding in the development of correct and reliable software. Event B method is based on set theory \\u0026amp; predicate logic, offering a mathematical base for rigorous system analysis. Event B models are separated into two basic components: contexts and machines. The context part describes the static part of the model, whereas the machine part describes the dynamic part, where all events are formalized step by step with the help of guards and actions. Event B allows the model to be developed step by step via mechanisms such as machine refinement and context extension.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp;Key aspects of Event B include events that represent state changes in the system, capturing the conditions under which an event can occur and the effect it has on the system state. The second aspect is refinement, where this process allows the gradual development of a system from an abstract specification to a concrete implementation. The next aspects of event b are theorems and proof obligations, this obligation ensures that the specified system properties hold at each refinement level, providing a systematic way to ensure correctness.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eF) Rodin Tool:\\u0026nbsp;\\u003c/strong\\u003eThe Rodin tool is a formal modeling platform designed for system development using the Event-B method. It provides a framework for creating and verifying complex systems through refinement and proof obligations. Built on an Eclipse-based integrated development environment (IDE), Rodin supports system behavior modeling using set theory and predicate logic. The tool automates the mathematical proof process, ensuring consistency across different abstraction levels. Its primary objective is to enable rigorous development of reliable and error-free software systems, making it a valuable resource for formal verification and validation [43] .\\u003c/p\\u003e\\n\\n\"},{\"header\":\"5. Event-B model of EPNN-based load balancing\",\"content\":\"\\u003cp\\u003eAfter introducing EPNN, ERAA, DDA, and RRAA, the Event B model of EPNN load balancing contains various invariants and events [44]. As we know, the Rodin tool has two parts- context and machines. Context’s part contains a set, constants, and axioms, where all the static parts of the model should be contained. In the sets part, we have declared the set of messages, node, coordinator, requests, status, etc. In constant part, we have declared underloaded, overloaded, request, reply, in progress, completed, etc. In the axioms part, we defined the definition of status where all type of load is declared of the node. In the case of message type, whenever it is requested, reply and minimum load. A mapping (mm↦nn) ∈ sender indicates that message mm is sent by the node nn. The machine part contains a dynamic part where variables, invariants, and events. Invariants define the definition of variables and initialize each variable in the events. Events refer to fundamental constructs used to model state transitions in the system. In the Rodin tool, events are a key component of event B models, providing a formal and systematic way to specify and analyze system behaviour.\\u003c/p\\u003e\\u003cp\\u003eThe machine part of the EPNN model like variables, invariants, and initialization as follows:\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eVariables:\\u003c/strong\\u003e clustergroup, nodegroup, sender, msgsend, messagetype, deliver, serverstatus, prerequesttable, servermanager, minloadmsg, replymsgrcd, requirementserver, selectedserver, patternmatching, clustercoordinator, PNNgroup, PNNcoordinator, nodeload, nodepriority\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eInitialization:\\u003c/strong\\u003e We declare all the initial values with ∅ a value, but some values cannot be null. Like serverstatus variable declared with an underloaded value. At the initial level, the status of the server must be declared as underloaded or overloaded.\\u003c/p\\u003e\\u003cp\\u003eA) The variable \\u003cem\\u003enodegroup\\u003c/em\\u003e is a subset of the NODE set (Inv1). Similarly, \\u003cem\\u003eclustergroup\\u003c/em\\u003e is a subset of CLUSTER set (Inv2). The variable \\u003cem\\u003esender\\u003c/em\\u003e sends the message from the request node shown in (Inv4).\\u003c/p\\u003e\\u003cp\\u003eB) Inv6 shows the type of message which is request, reply, and minimum load. Inv7 similarly represents the node status timein or timeout. Variable \\u003cem\\u003eserverstatus\\u003c/em\\u003e shows the status of the server underloaded, overloaded, and most appropriate (Inv9).\\u003c/p\\u003e\\u003cp\\u003eC) Variable \\u003cem\\u003erequestqueue\\u003c/em\\u003e is a bijective relation between nodes in set NODE and messages in set MESSAGE (Inv10). The receiver node receives the request message from the sender node and saves it in the request queue form of the table.\\u003c/p\\u003e\\u003cp\\u003eD) Inv13, replymsgsend represents the sending of a message from an underloaded node to an overloaded node.\\u003c/p\\u003e\\u003cp\\u003eE) The variable prerequesttable states that the function is a total function from the set REQUESTS to the set prereqstatus. The status of the pre-request table is already and not appropriate (NA). (Inv15)\\u003c/p\\u003e\\u003cp\\u003eF) Inv18, replymsgrcd shows the messages received by participating nodes from the corresponding node.\\u0026nbsp;\\u003c/p\\u003e\\u003cp\\u003eG) In Inv19, the statement suggests that a \\\"requirements server\\\" belongs to the set or type of nodes denoted by \\\"NODE,\\\" and it is related to or connected with a \\\"calculating server.\\\" The parameters of the calculating server are the predefined time, deadline time, and request size.\\u003c/p\\u003e\\u003cp\\u003eH) The variable \\u003cem\\u003epatternmatching\\u003c/em\\u003e shows that the selected server or node in the cluster matches all the requirements and provides either true or false. (Inv21)\\u003c/p\\u003e\\u003cp\\u003eI) Inv22 and Inv24 represent the clustercoordinator and PNN coordinator, where a new node is selected in the cluster group and PNN group and declared as a coordinator.\\u003c/p\\u003e\\u003cp\\u003eJ) Variable \\u003cem\\u003enodeload\\u0026nbsp;\\u003c/em\\u003eshows the load of the node, which is a natural number (Inv25). Variable \\u003cem\\u003enodepriority\\u003c/em\\u003e decides the priority of the node, which are either low or high (Inv26). Variable probscore represents the probability of all the nodes (Inv27), and selectnode represents the highest probability node that will be selected (Inv28). (See Fig2)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003e5.1 Events\\u003c/strong\\u003e\\u003c/p\\u003e\\u003cp\\u003eIn the previous section, we defined variables, invariants, and initialization of EPNN load balancing. Now we elaborate on the events in an effective probabilistic neural network process (EPNN). Events are a fundamental concept used to model the behaviour and changes in a system. Events are specified within the context of transition and modification. The initial event in the Rodin tool is typically named ‘INITIALIZATION’ and is responsible for setting up the initial state of the system. This event is automatically executed when the system starts. Create other events to capture state changes or actions within the system. These events should be defined with preconditions and postconditions, specifying the conditions under which the event can occur and the changes it makes to the system. Rodin generates proof obligations for each event, ensuring that the specified preconditions imply the postcondition and that the events preserve invariants.\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eA) Create clustergroup:\\u0026nbsp;\\u003c/strong\\u003eIn this event, the Rodin tool event \\\"Create ClusterGroup\\\" defines the creation of a new cluster group. It selects a node from the existing nodes, removes it from the \\\"nodegroup,\\\" and adds it to the \\\"clustergroup,\\\" ensuring the selected node is valid and not already in the cluster group.Node nn was removed from node group (act1) and added to cluster group (act2) (See Fig3).\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eB) Sending the request into cluster:\\u0026nbsp;\\u003c/strong\\u003eIn this event, \\\"Request will be sent into cluster\\\" models the process of sending a request message from a node in the \\\"clustergroup.\\\" When a node \\u003cem\\u003enn\\u003c/em\\u003e is selected from the cluster, and a new message \\u003cem\\u003emm\\u003c/em\\u003e is chosen, the event ensures that \\u003cem\\u003enn\\u003c/em\\u003e is a valid node, \\u003cem\\u003emm\\u003c/em\\u003e is not already in the set mess (grd4), and it has not been sent before by any node in the current sender domain (grd5). If conditions are met, the event updates the system state. It associates the message mm with the node \\u003cem\\u003enn\\u003c/em\\u003e in the sender domain (act1), sets the message type to \\\"request,\\\"(act2) updates the status of node \\u003cem\\u003enn\\u003c/em\\u003e to \\\"timeout,\\\"(act3), and records the message \\u003cem\\u003emm\\u003c/em\\u003e in the set ‘msgsend’(act4) and priority of node \\u003cem\\u003enn\\u003c/em\\u003e is low (See Fig4).\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eC) Declare the coordinator:\\u0026nbsp;\\u003c/strong\\u003eThe event is triggered when a condition is satisfied, including the presence of a cluster, the availability of a new node \\u003cem\\u003e(nn2\\u003c/em\\u003e), and the absence of a mapping between the current coordinator (\\u003cem\\u003ecc\\u003c/em\\u003e) and the new node in the “cluster coordinator” relation. The guard 4 present that node \\u003cem\\u003enn2\\u003c/em\\u003e is not declared yet as “cluster coordinator”. Node \\\"\\u003cem\\u003enn2\\u003c/em\\u003e\\\" in the system model must be less than or equal to a predefined threshold value (grd5). The action updates the “cluster coordinator” relation by assigning the new node \\u003cem\\u003e(nn2)\\u003c/em\\u003e as the coordinator for the specified cluster (\\u003cem\\u003ecc\\u003c/em\\u003e). (See Fig5)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eD) Delivery of Request message in coordinator node:\\u0026nbsp;\\u003c/strong\\u003eIn Fig6, the node \\u003cem\\u003enn\\u0026nbsp;\\u003c/em\\u003emust be part of the set of nodes (reqnodes) that are eligible to receive requests (grd1). The status of the node \\u003cem\\u003enn\\u003c/em\\u003e must be set to \\\"timeout,\\\" suggesting that the node is available for receiving a request (grd4). There should not be an existing mapping from node \\u003cem\\u003enn1\\u003c/em\\u003e to message \\u003cem\\u003emm\\u003c/em\\u003e in the deliver relation, indicating that this message has not been delivered to node \\u003cem\\u003enn1\\u003c/em\\u003e before (grd11). The combination of message \\u003cem\\u003emm\\u003c/em\\u003e and node \\u003cem\\u003enn\\u003c/em\\u003e should not exist in the requestqueue nn1 relation, ensuring that the request is not already in the processing queue (grd12). We declare node \\u003cem\\u003enn2\\u003c/em\\u003e is the coordinator from the previous event (grd13).\\u003c/p\\u003e\\u003cp\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp; The action updates the deliver relation by adding a new mapping from node \\u003cem\\u003enn1\\u003c/em\\u003e to message \\u003cem\\u003emm\\u003c/em\\u003e, indicating that the message has been delivered to node \\u003cem\\u003enn1\\u003c/em\\u003e (act1). In act2, the action updates the requestqueue relation by adding a new mapping from node \\u003cem\\u003enn1\\u003c/em\\u003e to a set containing a new mapping from message mm to node \\u003cem\\u003enn\\u003c/em\\u003e, indicating that a new request is added to the queue of node \\u003cem\\u003enn1\\u003c/em\\u003e. In act3, defines the message delivered within the time frame.\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eE) Nearest cloud will be chosen:\\u0026nbsp;\\u003c/strong\\u003eAfter delivery of the message into node \\u003cem\\u003enn1\\u003c/em\\u003e, the nearest cloud is selected for processing the request. In Fig7, message \\u003cem\\u003emm\\u003c/em\\u003e is successfully delivered in node \\u003cem\\u003enn1\\u003c/em\\u003e (grd7). Guard 8 represents the value \\u003cem\\u003eld\\u003c/em\\u003e must be a natural number, representing the load. The load value \\u003cem\\u003eld\\u003c/em\\u003e must be equal to the difference between the specified \\u003cem\\u003elvalue\\u0026nbsp;\\u003c/em\\u003eand a threshold, ensuring that the load is within a certain range (grd9). Node \\u003cem\\u003enn\\u003c/em\\u003e sends the message \\u003cem\\u003emm\\u003c/em\\u003e and saves it in the sender domain (grd10). The combination of the original request message \\u003cem\\u003emm\\u003c/em\\u003e and the new message m must not be in the domain of the replymsgsend relation, ensuring that this reply has not been recorded before (grd14). The new message\\u003cem\\u003e\\u0026nbsp;m\\u003c/em\\u003e and its load value\\u003cem\\u003e\\u0026nbsp;ld\\u003c/em\\u003e must not be in the load relation, ensuring that the load information has not been assigned yet (grd16) and the load of node \\u003cem\\u003enn1\\u003c/em\\u003e must not exceed a predefined threshold (grd17). If all the guards are true, then we perform some action according to our algorithm. In act1, the msgsend relation is updated by adding the new message \\u003cem\\u003em\\u003c/em\\u003e to the set of messages that have been sent. We define the type of message \\u003cem\\u003emm\\u003c/em\\u003e as ‘reply’ and update the replymsgsend relation by adding a new mapping from the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;m}\\u003c/em\\u003e to the node \\u003cem\\u003enn1\\u003c/em\\u003e, indicating that this reply is sent to node \\u003cem\\u003enn1\\u003c/em\\u003e (act2 \\u0026amp; 3). Updates the sender relation by assigning node \\u003cem\\u003enn1\\u0026nbsp;\\u003c/em\\u003eas the sender of the new message \\u003cem\\u003em\\u003c/em\\u003e and updates the load relation by assigning the load value \\u003cem\\u003eld\\u0026nbsp;\\u003c/em\\u003eto the new message \\u003cem\\u003em\\u003c/em\\u003e (act4 \\u0026amp; 5). The priority of node \\u003cem\\u003enn1\\u003c/em\\u003e is set to high.\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eF) If the request is already predefined:\\u0026nbsp;\\u003c/strong\\u003eIn this event, the value associated with request \\u003cem\\u003err\\u0026nbsp;\\u003c/em\\u003ein the prerequesttable relation must be \\\"already,\\\" indicating that this request has already been processed (grd6). In guard7, the combination of request \\u003cem\\u003err\\u0026nbsp;\\u003c/em\\u003eand its associated load value \\u003cem\\u003erld\\u0026nbsp;\\u003c/em\\u003emust not be in the server manager relation, ensuring that this request has not been assigned a load value in the server manager. Load value \\u003cem\\u003erld\\u0026nbsp;\\u003c/em\\u003emust be a natural number, representing the load to the request in the server manager(grd8). If all the guards are true, then the action updates the servermanager relation by adding a new mapping from the request \\u003cem\\u003err\\u0026nbsp;\\u003c/em\\u003eto its load value \\u003cem\\u003erld\\u003c/em\\u003e, assigning the load value to the request in the server manager. (See Fig8).\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eG) Send the reply to node from server manager:\\u0026nbsp;\\u003c/strong\\u003eIn this event, the reply message received from node \\u003cem\\u003enn\\u003c/em\\u003e into node \\u003cem\\u003enn1\\u003c/em\\u003e with message \\u003cem\\u003em,\\u003c/em\\u003e where the message type of \\u003cem\\u003em\\u003c/em\\u003e is minimum load represented with load value \\u003cem\\u003erld\\u003c/em\\u003e. In guard 7, the combination of the request\\u003cem\\u003e\\u0026nbsp;rr\\u003c/em\\u003e and its load value \\u003cem\\u003eld\\u003c/em\\u003e must be in the servermanager relation, indicating that this request has been assigned a load value. The combination of the pair {m\\u0026nbsp;↦\\u0026nbsp;rld} and \\u003cem\\u003enn1\\u003c/em\\u003e must be in the replymsgsend relation, indicating that a reply message has been sent to node \\u003cem\\u003enn1\\u003c/em\\u003e containing the minimum load message \\u003cem\\u003erld\\u003c/em\\u003e (grd11). Node \\u003cem\\u003enn1\\u003c/em\\u003e and the set \\u003cem\\u003e{m\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;rld}\\u003c/em\\u003e must not be in the replymsgrcd relation, indicating that this reply has not been recorded before for node \\u003cem\\u003enn1\\u003c/em\\u003e (grd12). If all the guards are true, action will be pursued according to the condition. In action, this event updates the replymsgrcd relation by adding a new mapping from node \\u003cem\\u003enn1\\u003c/em\\u003e to the set \\u003cem\\u003e{m\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;rld},\\u003c/em\\u003e recording the reception of the reply message by node \\u003cem\\u003enn1\\u003c/em\\u003e in\\u0026nbsp; the action field (act1). (See Fig9)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eH) If the request is not found in the server manager:\\u0026nbsp;\\u003c/strong\\u003eIn this event, we assume no server is found up to the mark then we send the request to other servers, that are situated in another cluster. The combination of request \\u003cem\\u003err\\u003c/em\\u003e and its load value \\u003cem\\u003erld\\u003c/em\\u003e must not be in the servermanager relation, ensuring that this request has not been assigned a load value in the server manager (grd5). If all requirements are fulfilled like predefined time, deadline time, and request size, then send the message into that cluster or server (grd6,7,8). The combination of the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;m}\\u003c/em\\u003e must not be in the domain of the replymsgsend relation, ensuring that this reply has not been recorded before and the message \\u003cem\\u003em\\u003c/em\\u003e must not be in the domain of the sender relation, indicating that it has not been assigned a sender yet (grd9 \\u0026amp; 10). In the action part, the action 1 updates the replymsgsend relation by adding a new mapping from the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;m}\\u003c/em\\u003e to the node \\u003cem\\u003enn1\\u003c/em\\u003e, indicating that a reply message containing the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;m}\\u003c/em\\u003e is sent to node \\u003cem\\u003enn1\\u003c/em\\u003e. (Act 1). In Act2, updates the sender relation by assigning node \\u003cem\\u003enn1\\u003c/em\\u003e as the sender of the message m and declaring the message type as a reply. (See Fig10)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eI) If the required capability is not matched with any server:\\u0026nbsp;\\u003c/strong\\u003eA new request will be sent in the cluster, but none of the cluster’s servers will match the essential requirement then we will divert the request into another cluster. In Fig11, nodes \\u003cem\\u003enn1\\u003c/em\\u003e and \\u003cem\\u003enn\\u003c/em\\u003e must represent a valid node (grd1 \\u0026amp;2). If none of the servers is capable of serving the request, then we choose the other cluster (See guard6,7,8). If we assume node \\u003cem\\u003enn1\\u003c/em\\u003e is overloaded and other nodes are also busy, choose the other one (guard 9). Variable \\u003cem\\u003enn2\\u003c/em\\u003e must be a set representing a valid subset of nodes and the set of nodes represented by \\u003cem\\u003enn2\\u003c/em\\u003e must not be a subset of the cluster group yet (grd10 \\u0026amp;11). If all the guards are true, then the action updates the “nodegroup” by removing the nodes represented by \\u003cem\\u003enn2\\u003c/em\\u003e from it (act1). In act2, the action updates the clustergroup by adding the nodes represented by \\u003cem\\u003enn2\\u003c/em\\u003e to it and setting the priority of node \\u003cem\\u003enn1\\u0026nbsp;\\u003c/em\\u003eas low (act3).\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eJ) Choose another appropriate cluster from all cluster groups:\\u0026nbsp;\\u003c/strong\\u003eFrom the previous event, if the required capability is not matched, then choose another cluster group’s node. In this event, we assume all the requirements are fulfilled by the server’s node and it is underloaded and accepts the load, then we will transfer the load. In Fig12, the variable \\u003cem\\u003enn2\\u003c/em\\u003e must represent a valid node in the system, and node \\u003cem\\u003enn2\\u0026nbsp;\\u003c/em\\u003emust be part of the cluster group (“clustergroup”) (grd1 \\u0026amp; 2). The requirement for the server at node \\u003cem\\u003enn2\\u003c/em\\u003e must be \\\"predefined time, deadlinetime \\u0026amp; requestsize is fulfilled shown in (grd5,6,7). The combination of node \\u003cem\\u003enn2\\u003c/em\\u003e and message mm must not be in the deliver relation, indicating that this message has not been delivered by node \\u003cem\\u003enn2\\u003c/em\\u003e yet (guard10). The combination of the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;nn}\\u003c/em\\u003e must not be in the requestqueue relation for node \\u003cem\\u003enn2\\u003c/em\\u003e, indicating that this request has not been queued for delivery by node \\u003cem\\u003enn2\\u003c/em\\u003e (guard11). If all the guards are true, accordingly action will be performed. In Act1, updates the deliver relation by adding a new mapping from node nn2 to message mm, indicating that node \\u003cem\\u003enn2\\u003c/em\\u003e delivers message \\u003cem\\u003emm\\u003c/em\\u003e. In acts 2 \\u0026amp; 3, update the requestqueue relation by adding a new mapping from node \\u003cem\\u003enn2\\u003c/em\\u003e to the set containing the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;nn},\\u003c/em\\u003e indicating that node \\u003cem\\u003enn2\\u003c/em\\u003e queues this delivery request and updates the server status of node \\u003cem\\u003enn2\\u003c/em\\u003e to \\\"mostappropriate\\\" for receiving the load and priority of node \\u003cem\\u003enn2\\u003c/em\\u003e is set to high.\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eK) Choosing the best server using round round-robin technique:\\u0026nbsp;\\u003c/strong\\u003eTo decide the best server, we choose the round-robin assignment technique. In this technique, if there is more than one request has the same arrival time value then the server manager will arrange them according to the turnaround time (TAT). In Fig13, the variable\\u003cem\\u003e\\u0026nbsp;ss\\u003c/em\\u003e must represent a valid server in the system (grd1). The server status of the node \\u003cem\\u003enn2\\u003c/em\\u003e must be \\\"most appropriate,\\\" indicating that this server is considered the most appropriate for the current operation in another cluster (grd2). The combination of node \\u003cem\\u003enn2\\u003c/em\\u003e and the set containing the pair \\u003cem\\u003e{mm\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;nn}\\u003c/em\\u003e must be in the “request queue” relation, indicating that this request is queued for delivery by node \\u003cem\\u003enn2\\u003c/em\\u003e (grd3). The server \\u003cem\\u003ess\\u0026nbsp;\\u003c/em\\u003emust not be in the set of selected servers, indicating that it has not been chosen in the current round-robin iteration. If all the guards are true then we choose the best server using round-robin techniques. This server must fulfill all the conditions like large request size, large predefined time, less deadline time, and less loaded one. In act1, the server \\u003cem\\u003ess\\u003c/em\\u003e must not be in the set of selected servers, indicating that it has not been chosen in the current round-robin iteration.\\u0026nbsp;\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eL)\\u0026nbsp;\\u003c/strong\\u003e\\u003cstrong\\u003eEPNN\\u0026nbsp;algorithm\\u0026nbsp;for\\u0026nbsp;selecting\\u0026nbsp;the\\u0026nbsp;best\\u0026nbsp;node:\\u003c/strong\\u003eIn this event, choosing best node belongs to the set of all available nodes (grd1). This guard (grd2) states that ss, which is the currently selected server, is being checked or compared in the process. It ensures consistency with the overall system state regarding server selection. In grd3, node \\u003cem\\u003enn3\\u003c/em\\u003e is less than or equal to a predefined threshold. The threshold represents the maximum load that a node can handle efficiently. Now guard 4 present the universally quantified guard condition. It ensures that for all nodes k that belong to the set of nodes (NODE), if their load is below the threshold, the probability score of node \\u003cem\\u003enn3\\u003c/em\\u003e is greater than or equal to the probability score of any other node k. In other words, \\u003cem\\u003enn3\\u003c/em\\u003e is selected because it has the highest probability score among all the nodes with a load below the threshold. In action, act1 updates the set selectnode by adding \\u003cem\\u003enn3\\u003c/em\\u003e to it (See Fig14)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eM) EPMNN Algorithm:\\u0026nbsp;\\u003c/strong\\u003eIn the previous event, we select the best server using the RR algorithm. After this, we matched all the conditions. If all the patterns are matched then selected node \\u003cem\\u003enn2\\u003c/em\\u003e makes them true. The \\\"Effective Probabilistic Matchmaking Neural Network Algorithm\\\" in load balancing is likely a sophisticated method that uses probabilistic matching, possibly facilitated by a neural network, to dynamically and optimally distribute computational workloads across servers in a network. The goal is to achieve efficient resource utilization, minimize response times, and enhance the overall performance of the distributed system. A neural network might be employed to dynamically adjust the assignment of tasks to servers based on real-time feedback and historical data. In Fig15, the variable \\u003cem\\u003ess\\u003c/em\\u003e represents a server that has been selected in the current context. The guard ensures that the server \\u003cem\\u003ess\\u0026nbsp;\\u003c/em\\u003eis indeed in the set of selected servers (grd1). The guard (grd2) checks that the server status of the node \\u003cem\\u003enn2\\u003c/em\\u003e is \\\"mostappropriate\\\" indicating that this server is considered the most appropriate for the current operation. In grd3, the guard checks that the current pattern-matching status for node \\u003cem\\u003enn3\\u003c/em\\u003e is set to \\\"probabilistic false,\\\" indicating that the pattern-matching process for this server is currently not activated or has not been marked as successful. In act1, action updates the pattern matching status for node \\u003cem\\u003enn3\\u003c/em\\u003e by assigning the value \\\"probabilistic true\\\" to it. This signifies that the pattern-matching process for this server has been successful or activated as a result of the probabilistic matchmaking algorithm\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eN) If a new request is not matched in the same server:\\u0026nbsp;\\u003c/strong\\u003eIf the matched server is not available in the same cluster, then we will find the next server by broadcasting the request message. The guard1 checks that the server ss is not already in the set of selected servers. This condition ensures that the server is not currently selected for the task. In grd2 \\u0026amp; grd3 ensure that variable \\u003cem\\u003ess2\\u003c/em\\u003e represents another server in the system. The guard ensures that \\u003cem\\u003ess2\\u003c/em\\u003e is a valid server and checks that the server \\u003cem\\u003ess2\\u003c/em\\u003e is already in the set of selected servers. This condition likely ensures that \\u003cem\\u003ess2\\u003c/em\\u003e is selected for the task. Grd4 checks that the pattern-matching status for node \\u003cem\\u003enn2\\u003c/em\\u003e is \\\"probabilistic false,\\\" indicating that the pattern-matching process for this server is not currently successful or activated. Guard 8 checks that the pattern-matching status for node \\u003cem\\u003enn3\\u003c/em\\u003e is \\\"probabilistic false,\\\" indicating that the pattern-matching process for this server is not currently successful or activated. Grd 10 and 11 shows that specifies that the computational load of node \\\"\\u003cem\\u003enn2\\u003c/em\\u003e\\\" must be equal to or greater than a predefined threshold and the computational load of node \\\"\\u003cem\\u003enn3\\u003c/em\\u003e\\\" must not exceed a predefined threshold. If all the guards are true, act1 updates the set of selected servers (“selectedserver”) by adding \\u003cem\\u003ess2\\u003c/em\\u003e to it. This signifies that \\u003cem\\u003ess2\\u003c/em\\u003e is now selected for the task. Act2 \\u0026amp; 3 represent that updates the nodegroup by removing \\u003cem\\u003enn3\\u0026nbsp;\\u003c/em\\u003efrom it. This likely means that \\u003cem\\u003enn3\\u003c/em\\u003e is no longer available for receiving tasks and updates the clustergroup by adding \\u003cem\\u003enn3\\u003c/em\\u003e. This likely means that nn3 is now part of a different cluster. Action4 \\u0026amp; 5 update the pattern matching status for node \\u003cem\\u003enn3\\u003c/em\\u003e by setting it to \\\"ptrue.\\\" This signifies that the pattern-matching process for this server is now successful or activated and it is underloaded for receiving the load of new requests. (See Fig16)\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eO) Make a probabilistic neural network (PNN) coordinator:\\u0026nbsp;\\u003c/strong\\u003eIn Fig17, after declaring node nn3 is suitable for processing the load of new requests then we will make a PNN coordinator for handling the request. A probabilistic neural network (PNN) in load balancing operates by leveraging statistical probabilities to distribute computational tasks across servers dynamically. It learns patterns from historical data to predict optimal servers, considering factors like server load, response times, and task requirements. The network probabilistically assigns tasks to servers based on learned correlations, aiming to achieve efficient resource utilization and minimize system bottlenecks. The guard grd4 checks that the pattern matching status for node nn3 is set to \\\"ptrue,\\\" indicating that this node has successfully undergone the pattern matching process, and grd3 presents that server node \\u003cem\\u003enn3\\u003c/em\\u003e has underloaded. Guard5 ensures that \\u003cem\\u003epp\\u003c/em\\u003e is a valid node representing a member of the Probabilistic Neural Network (PNN) group. Guard6 checks that the pair \\u003cem\\u003e(pp\\u0026nbsp;\\u003c/em\\u003e\\u003cem\\u003e↦\\u003c/em\\u003e\\u003cem\\u003e\\u0026nbsp;nn3)\\u0026nbsp;\\u003c/em\\u003eis not yet declared the PNN coordinator, ensuring that the selected PNN group pp is not already a coordinator. Previously, node \\u003cem\\u003enn2\\u003c/em\\u003e was the cluster coordinator (grd8). Guard9 checks that the nodes \\u003cem\\u003enn2\\u003c/em\\u003e and \\u003cem\\u003enn3\\u003c/em\\u003e are the same, ensuring that the selected coordinator node has the same properties as the specified node with potential PNN coordination. Guard 10 shows the server \\u003cem\\u003ess\\u003c/em\\u003e is the selected server. If all the guards are true, then we declare node \\u003cem\\u003enn3\\u003c/em\\u003e as PNN coordinator (act1).\\u003c/p\\u003e\\u003cp\\u003e\\u003cstrong\\u003eA summary of all events ensures that the specified Rodin tool events collectively describe a dynamic and adaptive load balancing system using probabilistic techniques and neural network concepts. The events cover various aspects of the load-balancing process, addressing server selection of minimum load, pattern matching, and coordination within clusters. The \\\"Effective Probabilistic Matchmaking Neural Network Algorithm\\\" event introduces probabilistic matching, utilizing neural network principles to assign tasks to servers efficiently. Another event ensures that if a server request is not matched, alternative servers are selected based on specific criteria. Moreover, the system dynamically designates new nodes as PNN (Probabilistic Neural Network) coordinators to handle load coordination, considering underloaded status, successful pattern matching, and cluster coordination. These events collectively depict a sophisticated and adaptive load balancing mechanism that optimizes resource utilization and minimizes bottlenecks in a dynamic computing environment.\\u003c/strong\\u003e\\u003c/p\\u003e\"},{\"header\":\"6. EPNN Load Balancing Validation with Metrics\",\"content\":\"\\u003cp\\u003eFor the validation process, we applied a probabilistic neural network (EPNN) model for load balancing across multiple servers. We take a dataset of 200 rows, where the dataset includes features like server status, data progress, network traffic, server load, and priority levels. The EPNN model aims to predict the optimal server (between s1 to s7) based on these features, ensuring balanced resource distribution and minimal latency. For output parameters, we calculate the predicted server and their probability between servers. The dataset was split into training (80%) and testing (20%) subsets using the hold-out validation technique. Features were normalized using Standard Scaler for better performance in the neural network. An MLP Classifier from Scikit-learn was used to model the EPNN, and prediction probabilities were output for each test sample. Best suitable server and all the parameters matched, we transfer the load to the respective server.\\u003c/p\\u003e \\u003cp\\u003eFor verification of the EPNN-based load balancing, we used the Event B platform with the Rodin tool. The tool generates the proof tree and proof obligation. Once the proof obligation is discharged and all the nodes in the proof tree are resolved, the proof obligation will be marked as proved. For validation, we implement a model in Python that calculates each server\\u0026rsquo;s criteria and predicts the server status and its probability. First, we data processing, feature selection, model training, and testing the prediction. This setup calculates each row\\u0026rsquo;s prediction individually and provides the server\\u0026rsquo;s name and probability score. The key advantage of EPNN in load balancing is fast training, probability decision, and real-time load balancing, which is crucial for dynamic load balancing in cloud environments where request arrivals are frequent. Once the EPNN model is trained using server performance data (network traffic, server load, priority levels). It can be tested on new data to evaluate its performance.\\u003c/p\\u003e\"},{\"header\":\"7. Result\",\"content\":\"\\u003cp\\u003eFor validation of the algorithm, Fig18 represents the predictions and probabilities for a test dataset in a load-balancing scenario using a machine learning model. A total of 40 samples were generated with server prediction and probabilities. Here is a breakdown of its contents:\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e1\\u003c/strong\\u003e. \\u003cstrong\\u003eSample X\\u003c/strong\\u003e: Each row corresponds to an individual test sample.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e2. Predicted Server\\u003c/strong\\u003e: The predicted server that the model has selected for each test sample. The servers are labeled as s1, s2, s3, etc., up to s7.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003e3. Probabilities\\u003c/strong\\u003e: This represents the probability distribution over all possible servers (s1 to s7) for each in EPNN, random forest, and logistic regression test samples. The values in the probability array are percentages that sum to 100, showing how confident the model is about selecting a sample server.\\u003c/p\\u003e\\n\\u003cp\\u003eThis result shows that the EPNN model is more efficient as compared to the random forest and logistic regression. EPNN was more accurate, making it better suited for predicting server assignments in complex load-balancing scenarios. EPNN offered more refined probability distributions, providing a clearer picture of the confidence in its predictions. This makes it especially useful when decisions are based on probabilistic reasoning. The EPNN model was better at capturing intricate patterns in the data, thanks to its deep learning architecture. In contrast, random forest and logistic regression struggled to handle more complex, non-linear relationships.\\u003c/p\\u003e\\n\\n\\u003cp\\u003e\\u003cstrong\\u003eClassification Report of the EPNN model:\\u003c/strong\\u003e\\u0026nbsp; \\u0026nbsp; \\u0026nbsp; \\u0026nbsp;\\u003c/p\\u003e\\n\\u003ctable border=\\\"1\\\" cellspacing=\\\"0\\\" cellpadding=\\\"0\\\" width=\\\"553\\\"\\u003e\\n \\u003ctbody\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eClassification Parameter\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003ePrecision\\u0026nbsp;\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eRecall\\u0026nbsp;\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003e\\u0026nbsp;F1-score \\u0026nbsp; \\u0026nbsp;\\u0026nbsp;\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eSupport\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003eClass 0 (Low Priority)\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.56\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.67\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.61\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e128\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003eClass 1 (High Priority)\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.57\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.46\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.51\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e123\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003eAccuracy\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e-\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e-\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.56\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e251\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003eMacro Avg\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.57\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.56\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.56\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e251\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003eWeighted Avg\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.57\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.57\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e0.56\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20%;\\\"\\u003e\\n \\u003cp\\u003e251\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003c/tbody\\u003e\\n\\u003c/table\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eTable 1: Classification report of the EPNN model\\u003c/strong\\u003e\\u003cstrong\\u003e.\\u003c/strong\\u003e\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003eThe model\\u0026apos;s overall accuracy was 56%, indicating moderate performance in distinguishing between low-priority and high-priority requests. The precision for Class 1 (High Priority) was 0.57, meaning 57% of the instances predicted as high priority were correct. However, the recall for Class 1 was lower (0.46), indicating that the model missed 54% of actual high-priority cases.\\u003c/p\\u003e\\n\\u003cp\\u003eThe macro average F1-score (0.56) suggests that the model maintains a relatively balanced performance across both classes, but there is room for improvement in recall. The weighted average F1-score (0.56) confirms that the model performs similarly across different class distributions. (See Table1)\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eAUC-ROC Analysis\\u003c/strong\\u003e\\u003c/p\\u003e\\n\\u003cp\\u003eTo further evaluate the model\\u0026rsquo;s discriminative ability, the AUC-ROC score was computed. The model achieved an AUC-ROC score of 0.56, indicating slightly better-than-random classification performance.\\u003c/p\\u003e\\n\\u003cp\\u003eTo verify the algorithm, we implement an effective probabilistic neural network (EPNN) model in the Rodin tool. This model predicts server assignments for incoming requests. EPNNs are structured as neural networks, typically consisting of input, hidden, and output layers. The input layer receives features related to server load, threshold time, predefined time, deadline time, and request size. The hidden layer processes through interconnect nodes, and finally, the output layer generates a prediction of the optimal server assignment based on the learned patterns. After designing the model of EPNN load balancing, we implemented the events into the Event B tool on the RODIN platform for verification. All the events in the system are verified and validated with the Event B model. This model generates the proof obligations methods, which are manually or automatically discharged. Rodin tool generates a total of 122 proof obligations, 90 of which are discharged automatically, and 32 of which require manual interaction. (See Table 2)\\u003c/p\\u003e\\n\\u003ctable border=\\\"1\\\" cellspacing=\\\"0\\\" cellpadding=\\\"0\\\" align=\\\"\\\"\\u003e\\n \\u003ctbody\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 19.5079%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eElement name\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.3866%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eTotal P.O.\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eAutomatic P.O.\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eReviewed\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e\\u003cstrong\\u003eDischarged\\u003c/strong\\u003e\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 19.5079%;\\\"\\u003e\\n \\u003cp\\u003eContext\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.3866%;\\\"\\u003e\\n \\u003cp\\u003e0\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e0\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e0\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e0\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003ctr\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 19.5079%;\\\"\\u003e\\n \\u003cp\\u003eMachine\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.3866%;\\\"\\u003e\\n \\u003cp\\u003e112\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e90\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e22\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003ctd valign=\\\"top\\\" style=\\\"width: 20.0351%;\\\"\\u003e\\n \\u003cp\\u003e0\\u003c/p\\u003e\\n \\u003c/td\\u003e\\n \\u003c/tr\\u003e\\n \\u003c/tbody\\u003e\\n\\u003c/table\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eTable 2: Proof obligations generated by the Rodin tool\\u003c/strong\\u003e\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003eIn model training and testing, despite Random Forest being faster and easier to train, EPNN proved to be more efficient in scenarios that require deeper insights and more precise predictions. For tasks such as server load balancing, where decisions can be critical and misclassifications costly, EPNN provides a better solution. EPNN finds the probability of transferring the load nearly 90%, while the Random Forest algorithm finds the correct server less than 40%. So, the difference is clear, the probabilistic neural network is more accurate and efficient for transferring the large dynamic load in cloud servers. The proposed EPNN-based load balancing algorithm advances the state of the art by addressing key challenges in dynamic and large-scale cloud environments. Unlike traditional load balancing solutions, which often rely on static rules or heuristics, the EPNN approach leverages probabilistic neural networks (PNNs) for advanced prediction capabilities. This enables the system to anticipate server load trends and proactively redistribute requests, reducing response times and preventing overload scenarios. The integration of probabilistic models provides robust decision-making under uncertainty. The critical enhancement is in environments with unpredictable workload patterns.\\u003c/p\\u003e\"},{\"header\":\"8. Conclusion\",\"content\":\"\\u003cp\\u003eThis research proposes a forward-looking approach to load balancing in cloud computing by integrating Effective Probabilistic Neural Networks (EPNN) with formal modeling techniques such as Event-B. In cloud environments, data is growing day by day. We have proposed a methodology that aims to meet future demands by leveraging machine learning-driven mechanisms, including probabilistic matchmaking and intelligent data discovery, to dynamically and efficiently distribute workloads. The use of formal verification through the Event-B method and the Rodin tool ensures that the system remains logically sound and robust, even under rapidly changing conditions, thereby paving the way for high-reliability cloud infrastructures. Looking ahead, the incorporation of algorithms such as the Round Robin Assigning Algorithm (RRAA), Data Discovery Algorithm (DDA), and External Resource Access Algorithm (ERAA) positions the model to adapt seamlessly to future challenges like resource heterogeneity, increased demand, and real-time responsiveness. This makes the proposed solution not only scalable and efficient but also future-ready for evolving cloud computing ecosystems. This research bridges the gap between theoretical modeling and practical application by addressing real-world challenges in cloud-based load balancing. The proposed EPNN algorithm, verified through formal modeling, adapts dynamically to server conditions, making it suitable for commercial cloud environments like AWS, Microsoft Azure or private cloud. By optimizing resource usage and reducing processing delays, the model enhances user experience and lowers operational costs, offering a scalable and energy-efficient solution for next-generation data centers. In real-world deployment scenarios, the proposed approach can significantly reduce task response time, avoid server overloads, and optimize resource utilization, leading to improved quality of service (QoS) and enhanced user satisfaction.\\u003c/p\\u003e\"},{\"header\":\"Declarations\",\"content\":\"\\u003cp\\u003e\\u003cstrong\\u003eAcknowledgments:\\u003c/strong\\u003e The author extends their gratitude to the Rajkiya Engineering College, Banda for their invaluable continuous support for this research work.\\u0026nbsp;\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eAuthor contributions:\\u003c/strong\\u003e Shantanu Shukla (Corresponding Author): conceptualization, data curation, investigation, methodology, formal analysis, writing—original draft. Vibhash Yadav: reviewing and editing.\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eCorresponding author:\\u0026nbsp;\\u003c/strong\\u003eCorrespondence toShantanu Shukla\\u003c/p\\u003e\\n\\u003cp\\u003eEthics Declarations\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eFunding Declaration:\\u003c/strong\\u003e No funding\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eEthics and Consent to Participate declarations:\\u003c/strong\\u003e Not applicable\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eData Availability:\\u003c/strong\\u003e The datasets generated and analysed during the current study are available in the https://www.kaggle.com/datasets/shantanushukla2207/load-balancing-dataset\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eConsent to Publish declaration:\\u0026nbsp;\\u003c/strong\\u003enot applicable\\u003c/p\\u003e\\n\\u003cp\\u003e\\u003cstrong\\u003eCompeting Interest declaration:\\u003c/strong\\u003e The authors declare no competing interests\\u003c/p\\u003e\"},{\"header\":\"References\",\"content\":\"\\u003col\\u003e\\n\\u003cli\\u003eAli.F \\u0026amp; Khan.R, \\u0026ldquo;The study on load balancing strategies in distributed computing system\\u0026rdquo;, IJCSES, vol.3 no.2, page no. 19-30, 2012, DOI: 10.5121/ijcses.2012.3203\\u003c/li\\u003e\\n\\u003cli\\u003eAnna. Hac, \\u0026ldquo;Load balancing in distributed systems: A survey\\u0026rdquo; , AT \\u0026amp; T bell laboratories, Performance Evaluation Review, Vol. 16 dated on 2-4 February 1989 \\u003c/li\\u003e\\n\\u003cli\\u003eOthman.O \\u0026amp; Douglas.C., \\u0026ldquo;Optimizing distributed system performance via adaptive middleware load balancing\\u0026rdquo;, University of California, April 2001\\u003c/li\\u003e\\n\\u003cli\\u003eTyagi.V \\u0026amp; Tarun kr., \\u0026ldquo;ORT Broker Policy: Reduce Cost and Response Time Using Throttled Load Balancing Algorithm\\u0026rdquo;, Procedia Computer Science, Volume 48, 2015, Pages 217-221\\u003c/li\\u003e\\n\\u003cli\\u003eD. A. Shafiq, N. Jhanjhi, and A. Abdullah, \\u0026ldquo;Proposing A Load Balancing Algorithm for the Optimization of Cloud Computing Applications,\\u0026rdquo; MACS 2019 - 13th Int. Conf. Math. Actuar. Sci. Comput. Sci. Stat. Proc., 2019, doi: 10.1109/MACS48846.2019.9024785. \\u003c/li\\u003e\\n\\u003cli\\u003eVioletta N. Volkova et.al. \\u0026ldquo;Load balancing in cloud computing\\u0026rdquo;, 2018 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus), Jan 2018, IEEE, DOI: 10.1109/EIConRus.2018.8317113\\u003c/li\\u003e\\n\\u003cli\\u003eCaterina urban and Antoine Mine, \\u0026ldquo;A review of formal methods applied to machine learning\\u0026rdquo;, arXiv:2104.02466v2 [cs.PL] 21 Apr 2021\\u003c/li\\u003e\\n\\u003cli\\u003eEmre Gures et.al. \\u0026ldquo;Machine Learning-Based Load Balancing Algorithms in Future Heterogeneous Networks: A Survey\\u0026rdquo; IEEE Access Vol 10, Page 37689-37717, DOI: 10.1109/ACCESS.2022.3161511\\u003c/li\\u003e\\n\\u003cli\\u003eR. Agrawal, D.K. Sharma et.al. \\u0026ldquo;Machine learning and deep learning based load balancing algorithms techniques in cloud computing\\u0026rdquo;, 2021 International Conference on Innovative Practices in Technology and Management (ICIPTM), IEEE, April 2021, DOI: 10.1109/ICIPTM52218.2021.9388349\\u003c/li\\u003e\\n\\u003cli\\u003eX. Hou and G. Zhao, \\u0026quot;Resource Scheduling and Load Balancing Fusion Algorithm with Deep Learning Based on Cloud Computing\\u0026quot;, International Journal of Information Technology and Web Engineering (IJITWE), vol. 13, no. 3, pp. 54-72, 2018.\\u003c/li\\u003e\\n\\u003cli\\u003eC. Gomez, A. Shami and X. Wang, \\u0026quot;Machine Learning Aided Scheme for Load Balancing in Dense IoT Networks\\u0026quot;, Sensors, vol. 18, no. 11, pp. 3779, 2018.\\u003c/li\\u003e\\n\\u003cli\\u003eS. Parida and B. Panchal, \\u0026quot;An efficient dynamic load balancing algorithm using machine learning technique in cloud environment\\u0026quot;, International journal of scientific research in science engineering and technology, vol. 4, pp. 1184-1186, 2018.\\u003c/li\\u003e\\n\\u003cli\\u003eS. Moreno-Alvarez, J. M. Haut, M. E. Paoletti, J. A. Rico-Gallego, J. C. Diaz-Martin and J. Plaza, \\u0026quot;Training deep neural networks: a static load balancing approach\\u0026quot;, The Journal of Super computing, vol. 76, no. 12, pp. 9739-9754, 2020.\\u003c/li\\u003e\\n\\u003cli\\u003eThai Son Hoang, Jean Raymond Abrial \\u0026ldquo;Event-B Patterns and Their Tool Support\\u0026rdquo;, Software and Systems Modelling, May 2013, Vol 12 , issue 2, pp 229-244\\u003c/li\\u003e\\n\\u003cli\\u003eButler, Michael, Philipp K\\u0026ouml;rner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. \\u0026quot;The first twenty-five years of industrial use of the B-method.\\u0026quot; In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209. Springer, Cham, 2020.\\u003c/li\\u003e\\n\\u003cli\\u003eButler, Michael. \\u0026quot;Decomposition structures for Event-B.\\u0026quot; In International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009.\\u003c/li\\u003e\\n\\u003cli\\u003eAbrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. \\u0026quot;Rodin: an open toolset for modelling and reasoning in Event-B.\\u0026quot; International journal on software tools for technology transfer 12, no. 6 (2010): 447-466.\\u003c/li\\u003e\\n\\u003cli\\u003eNada M. Al Sallami et.al. \\u0026ldquo;Load balancing with Neural Network\\u0026rdquo;, The science and Information Organization, Volume 4 Issue 10, 2013, DOI: 10.14569/IJACSA.2013.041021\\u003c/li\\u003e\\n\\u003cli\\u003eSergio Moreno‑\\u0026Aacute;lvarez et.al. \\u0026ldquo;Training deep neural networks: a static load balancing approach\\u0026rdquo; The journal of supercomputing, Springer Nature 2020, https://doi.org/10.1007/s11227-020-03200-6\\u003c/li\\u003e\\n\\u003cli\\u003eMadhukar Prashant Shukla, Poonam Keswani, and Bright Keswani, \\u0026ldquo;Artificial neural network based load balancing scheme for top of rack switches in optical data centers\\u0026rdquo; Journal of Optical Communications, Published online by De Gruyter August 3, 2023, https://doi.org/10.1515/joc-2023-0189\\u003c/li\\u003e\\n\\u003cli\\u003eWaldemar pokuta, Krzysztof Zatwarnicki, \\u0026ldquo;Application of Neural Networks in Distribution of the Load in Cluster-Based Web Systems\\u0026rdquo; Web Infrastructure Enhancement and Performance Evaluation, Appl. Sci. 2022, 12(1), 79; https://doi.org/10.3390/app12010079\\u003c/li\\u003e\\n\\u003cli\\u003eShantanu shukla, Raghuraj singh, Divakar Yadav, \\u0026ldquo;Formal Modelling of Cluster-Coordinator-Based Load Balancing Protocol Using Event-B\\u0026rdquo;, Proceedings of Second Doctoral Symposium on Computational Intelligence, pp-593-603, vol: 1374, Singapore. https://doi.org/10.1007/978-981-16-3346-1_48\\u003c/li\\u003e\\n\\u003cli\\u003ePooja Yadav, Raghuraj Suryavanshi, Divakar Yadav, \\u0026ldquo;Formal Verification of Receiver Initiated Load Distribution Protocol with Fault Tolerance and Recovery using Event-B\\u0026rdquo;, Journal of Scientific and Industrial Research (JSIR), Vol:80 issue: 12, April 2022, pp:1078-1090\\u003c/li\\u003e\\n\\u003cli\\u003eBehshad Mohebali et. Al., \\u0026ldquo;Probabilistic neural networks: a brief overview of theory, implementation, and application, Handbook of Probabilistic Models. https://doi.org/10.1016/B978-0-12-816514-0.00014-X, year- 2012\\u003c/li\\u003e\\n\\u003cli\\u003eFatma M. Talaat, Ahmed Ibrahim Saleh, Hesham Arafat Ali, \\u0026ldquo;Effective Load Balancing Strategy (ELBS) for Real-Time Fog Computing Environment Using Fuzzy and Probabilistic Neural Networks, Journal of Network and Systems Management \\u0026middot; October 2019, https://www.researchgate.net/publication/330916938\\u003c/li\\u003e\\n\\u003cli\\u003eResat Umit Payli, Kayhan Erciyes, Orhan Dagdeviren, \\u0026ldquo;Cluster based load balancing algorithms for grids\\u0026rdquo;, International Journal of Computer Networks \\u0026amp; Communications (IJCNC) Vol.3, No.5, Sep 2011\\u003c/li\\u003e\\n\\u003cli\\u003ePrabhdeep Singh et.al., \\u0026ldquo;A fog based cluster based load balancing\\u0026rdquo;, S\\u003cem\\u003eustainability\\u003c/em\\u003e 14, no. 13: 7961. https://doi.org/10.3390/su14137961\\u003c/li\\u003e\\n\\u003cli\\u003eAnnaVictoria C R Oikawa, Vinicius Freitas, M\\u0026aacute;rcio C Castro, La\\u0026eacute;rcio Lima Pilla, \\u0026ldquo;Adaptive Load Balancing based on Machine Learning for Iterative Parallel Applications\\u0026rdquo;, Submitted on 12 May 2020, https://hal.science/hal-02570549\\u003c/li\\u003e\\n\\u003cli\\u003eChen, Shenghui \\u0026amp; Fan, Zhiming \\u0026amp; Shen, Haiying \\u0026amp; Feng, Lu. (2019). Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods. 146-151. 10.1109/MASSW.2019.00036.\\u003c/li\\u003e\\n\\u003cli\\u003eS. Chen, Z. Fan, H. Shen and L. Feng, \\u0026quot;Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods,\\u0026quot; \\u003cem\\u003e2019 IEEE 16th International Conference on Mobile Ad Hoc and Sensor Systems Workshops (MASSW)\\u003c/em\\u003e, Monterey, CA, USA, 2019, pp. 146-151, doi: 10.1109/MASSW.2019.00036\\u003c/li\\u003e\\n\\u003cli\\u003eEdwin ablad, \\u0026ldquo;Mathematical modelling and methods for load balancing and coordination of multi robot stations\\u0026rdquo;, Sweden 2022\\u003c/li\\u003e\\n\\u003cli\\u003eKai Zhang, Wei Guo, Jian Feng, \\u0026ldquo;Load Forecasting Method Based on Improved Deep Learning in Cloud Computing Environment\\u0026rdquo;, Scientific Programming Towards a Smart World: Hindawi Publication, Volume 2021, https://doi.org/10.1155/2021/3250732\\u003c/li\\u003e\\n\\u003cli\\u003eE. Gures, I. Shayea, M. Ergen, M. H. Azmi and A. A. El-Saleh, \\u0026quot;Machine Learning-Based Load Balancing Algorithms in Future Heterogeneous Networks: A Survey,\\u0026quot; in IEEE Access, vol. 10, pp. 37689-37717, 2022, doi: 10.1109/ACCESS.2022.3161511.\\u003c/li\\u003e\\n\\u003cli\\u003eMUHAMMAD ASIM SHAHID, NOMAN ISLAM et.al., \\u0026ldquo;A Comprehensive Study of Load Balancing Approaches in the Cloud Computing Environment and a Novel Fault Tolerance Approach\\u0026rdquo; IEEE Access, Accepted by 4 July, 2020, Digital Object Identifier 10.1109/ACCESS.2020.3009184\\u003c/li\\u003e\\n\\u003cli\\u003eM. Talaat, Fatma \\u0026amp; Ali, Hesham \\u0026amp; Saraya, Mohamed \\u0026amp; Saleh, Ahmed. (2022). Effective scheduling algorithm for load balancing in fog environment using CNN and MPSO. Knowledge and Information Systems. 64. 1-25. 10.1007/s10115-021-01649-2.\\u003c/li\\u003e\\n\\u003cli\\u003eMalavika, R. \\u0026amp; Valarmathi, M.. (2022). Adaptive Server Load Balancing in SDN Using PID Neural Network Controller. Computer Systems Science and Engineering. 42. 229-243. 10.32604/csse.2022.020947.\\u003c/li\\u003e\\n\\u003cli\\u003eKaur, Amanpreet \\u0026amp; Kaur, Bikrampal \\u0026amp; Singh, Parminder \\u0026amp; Devgan, Mandeep \\u0026amp; Toor, Harpreet. (2020). Load Balancing Optimization Based on Deep Learning Approach in Cloud Environment. International Journal of Information Technology and Computer Science. 12. 8-18. 10.5815/ijitcs.2020.03.02.\\u003c/li\\u003e\\n\\u003cli\\u003eYao, Zhiyuan \\u0026amp; Desmouceaux, Yoann \\u0026amp; Townsley, William \\u0026amp; Clausen, Thomas Heide. (2021). Towards Intelligent Load Balancing in Data Centers. https://doi.org/10.48550/arXiv.2110.15788\\u003c/li\\u003e\\n\\u003cli\\u003eL. Xu, H. H. Hoos, and K. Leyton-Brown. Hierarchical hardness models for SAT. In Conference on Principles and Practice of Constraint Programming, 2007\\u003c/li\\u003e\\n\\u003cli\\u003eL. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown. Satzilla: Portfolio-based algorithm selection for sat. JAIR, 32:565\\u0026ndash;606, 2008\\u003c/li\\u003e\\n\\u003cli\\u003eS. Tetsuya, A. Alejandra, B. Gilles et. Al, \\u0026ldquo;Formal Verification of Higher-order probabilistic programming\\u0026rdquo; (Reasoning about approximation), arxiv: 1807.06091V3[cs. L0] 25 Feb 2020\\u003c/li\\u003e\\n\\u003cli\\u003ePoppleton, M. (2008). The Composition of Event-B Models. In: B\\u0026ouml;rger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_17\\u003c/li\\u003e\\n\\u003cli\\u003eAbrial, JR., Butler, M., Hallerstede, S. et al. Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer 12, 447\\u0026ndash;466 (2010). https://doi.org/10.1007/s10009-010-0145-y\\u003c/li\\u003e\\n\\u003cli\\u003eDonald F. Specht, \\u0026ldquo;Probabilistic neural networks\\u0026rdquo;, Neural Networks, Volume 3, Issue 1, 1990, Pages 109-118, ISSN 0893-6080, https://doi.org/10.1016/0893-6080(90)90049-Q.\\u003c/li\\u003e\\n\\u003c/ol\\u003e\"}],\"fulltextSource\":\"\",\"fullText\":\"\",\"funders\":[],\"hasAdminPriorityOnWorkflow\":false,\"hasManuscriptDocX\":true,\"hasOptedInToPreprint\":true,\"hasPassedJournalQc\":\"\",\"hasAnyPriority\":false,\"hideJournal\":false,\"highlight\":\"\",\"institution\":\"\",\"isAcceptedByJournal\":true,\"isAuthorSuppliedPdf\":false,\"isDeskRejected\":\"\",\"isHiddenFromSearch\":false,\"isInQc\":false,\"isInWorkflow\":false,\"isPdf\":false,\"isPdfUpToDate\":true,\"isWithdrawnOrRetracted\":false,\"journal\":{\"display\":true,\"email\":\"info@researchsquare.com\",\"identity\":\"discover-computing\",\"isNatureJournal\":false,\"hasQc\":true,\"allowDirectSubmit\":false,\"externalIdentity\":\"\",\"sideBox\":\"Learn more about [Discover Computing](https://link.springer.com/journal/10791)\",\"snPcode\":\"10791\",\"submissionUrl\":\"https://submission.springernature.com/new-submission/10791/3\",\"title\":\"Discover Computing\",\"twitterHandle\":\"\",\"acdcEnabled\":true,\"dfaEnabled\":true,\"editorialSystem\":\"stoa\",\"reportingPortfolio\":\"Discover Series\",\"inReviewEnabled\":true,\"inReviewRevisionsEnabled\":true},\"keywords\":\"Load balancing, Cloud computing, Formal modelling, Probabilistic Neural Network, Event-B\",\"lastPublishedDoi\":\"10.21203/rs.3.rs-6006596/v1\",\"lastPublishedDoiUrl\":\"https://doi.org/10.21203/rs.3.rs-6006596/v1\",\"license\":{\"name\":\"CC BY 4.0\",\"url\":\"https://creativecommons.org/licenses/by/4.0/\"},\"manuscriptAbstract\":\"\\u003cp\\u003eLoad balancing plays a crucial role in distributed and cloud computing by evenly distributing workloads across multiple servers or network resources, ensuring optimal performance and resource utilization. It improves system reliability, fault tolerance, and response time by preventing overloading and rerouting tasks from failed or underperforming resources. This paper explores advanced load balancing techniques, focusing on machine learning integration for better handling imbalanced data and task distribution. We introduce an Effective Probabilistic Neural Network (EPNN) model that selects the best cluster for load distribution. Complementing this, we propose a Round Robin Assigning Algorithm (RRAA) for task allocation and a Data Discovery Algorithm (DDA) for identifying optimal nodes or clusters. The EPNN model\\u0026rsquo;s accuracy is verified through formal modeling using the Event-B tool, ensuring the correctness of the algorithm via automated and manual proof generation. This research aims to optimize load balancing in neural network environments, offering the highest probability algorithm for efficient resource management.\\u003c/p\\u003e\",\"manuscriptTitle\":\"Formal Modelling and Verification of Effective Probabilistic Neural Networks for Load Balancing in a Cloud Environment\",\"msid\":\"\",\"msnumber\":\"\",\"nonDraftVersions\":[{\"code\":1,\"date\":\"2025-04-24 02:50:38\",\"doi\":\"10.21203/rs.3.rs-6006596/v1\",\"editorialEvents\":[{\"type\":\"communityComments\",\"content\":0},{\"type\":\"editorAssigned\",\"content\":\"\",\"date\":\"2025-05-20T14:30:47+00:00\",\"index\":\"\",\"fulltext\":\"\"},{\"type\":\"decision\",\"content\":\"Revision requested\",\"date\":\"2025-05-20T14:30:23+00:00\",\"index\":\"\",\"fulltext\":\"\"},{\"type\":\"editorInvitedReview\",\"content\":\"\",\"date\":\"2025-05-13T07:28:24+00:00\",\"index\":\"hide\",\"fulltext\":\"\"},{\"type\":\"editorInvitedReview\",\"content\":\"\",\"date\":\"2025-04-22T11:25:58+00:00\",\"index\":\"hide\",\"fulltext\":\"\"},{\"type\":\"reviewerAgreed\",\"content\":\"101208999289452090276705971261876157350\",\"date\":\"2025-04-22T10:46:54+00:00\",\"index\":\"hide\",\"fulltext\":\"\"},{\"type\":\"reviewerAgreed\",\"content\":\"279009680293000047264230791950022663675\",\"date\":\"2025-04-22T10:36:22+00:00\",\"index\":\"hide\",\"fulltext\":\"\"},{\"type\":\"reviewersInvited\",\"content\":\"\",\"date\":\"2025-04-22T10:10:53+00:00\",\"index\":\"\",\"fulltext\":\"\"},{\"type\":\"checksComplete\",\"content\":\"\",\"date\":\"2025-04-22T09:49:59+00:00\",\"index\":\"\",\"fulltext\":\"\"},{\"type\":\"submitted\",\"content\":\"Discover Computing\",\"date\":\"2025-04-20T10:59:42+00:00\",\"index\":\"\",\"fulltext\":\"\"}],\"status\":\"published\",\"journal\":{\"display\":true,\"email\":\"info@researchsquare.com\",\"identity\":\"discover-computing\",\"isNatureJournal\":false,\"hasQc\":true,\"allowDirectSubmit\":false,\"externalIdentity\":\"\",\"sideBox\":\"Learn more about [Discover Computing](https://link.springer.com/journal/10791)\",\"snPcode\":\"10791\",\"submissionUrl\":\"https://submission.springernature.com/new-submission/10791/3\",\"title\":\"Discover Computing\",\"twitterHandle\":\"\",\"acdcEnabled\":true,\"dfaEnabled\":true,\"editorialSystem\":\"stoa\",\"reportingPortfolio\":\"Discover Series\",\"inReviewEnabled\":true,\"inReviewRevisionsEnabled\":true}}],\"origin\":\"\",\"ownerIdentity\":\"aa3cfdaa-fd54-490f-96f6-4518f209aa16\",\"owner\":[],\"postedDate\":\"April 24th, 2025\",\"published\":true,\"recentEditorialEvents\":[],\"rejectedJournal\":[],\"revision\":\"\",\"amendment\":\"\",\"status\":\"published-in-journal\",\"subjectAreas\":[],\"tags\":[],\"updatedAt\":\"2025-10-20T16:03:53+00:00\",\"versionOfRecord\":{\"articleIdentity\":\"rs-6006596\",\"link\":\"https://doi.org/10.1007/s10791-025-09748-2\",\"journal\":{\"identity\":\"discover-computing\",\"isVorOnly\":false,\"title\":\"Discover Computing\"},\"publishedOn\":\"2025-10-15 15:58:15\",\"publishedOnDateReadable\":\"October 15th, 2025\"},\"versionCreatedAt\":\"2025-04-24 02:50:38\",\"video\":\"\",\"vorDoi\":\"10.1007/s10791-025-09748-2\",\"vorDoiUrl\":\"https://doi.org/10.1007/s10791-025-09748-2\",\"workflowStages\":[]},\"version\":\"v1\",\"identity\":\"rs-6006596\",\"journalConfig\":\"researchsquare\"},\"__N_SSP\":true},\"page\":\"/article/[identity]/[[...version]]\",\"query\":{\"redirect\":\"/article/rs-6006596\",\"identity\":\"rs-6006596\",\"version\":[\"v1\"]},\"buildId\":\"8U1c8b4HqxoKbykW_rLl7\",\"isFallback\":false,\"isExperimentalCompile\":false,\"dynamicIds\":[84888],\"gssp\":true,\"scriptLoader\":[]}","source_license":"CC-BY-4.0","license_restricted":false}