# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 1 Introduction
As a result, it is important not only to recognize the various fault modes, as well as their primary triggers and complications, but also to apply real-time automatic fault monitoring tools that can stop the fault progression and reduce the need for corrective measures. A fault in the electric power system is ordinarily related to the abnormal supply of electric current, such as short-circuits. Several works have been completed in this field. In [2], formal verification of fault detection and mitigation in distribution automation was conducted using the Uppaal integrated tool environment. The author in [3] used the smart grids laboratory for the evaluation of the quality of service of the fault location, isolation, and service restoration functionalities. In [4], the author proposed an intelligent control system for fault identification in the distribution network using neural networks. While several mechanisms have been followed for monitoring, detecting, and isolating the faults in smart grids, the primary objective here is to design and model a fault-free distribution management system using IoT and finite automata in an efficient, reliable, and sustainable manner. In this paper, the aim is to improve the distribution management system of the smart grid using formal methods and a design model for fault identification, isolation, and service restoration in distribution management systems. The major objective is to formalize the model in an efficient way before its implementation so that there is less chance of errors during the implementation due to its validation in the formalizing phase. Fault identification detects all possible fault points; Fault Isolation identifies the best switching order sequence to isolate the fault; Service Restoration identifies the best switching order sequence to return power to the feeders' safe parts. Formal methods are abstract techniques that are used to model complex and sophisticated systems. Developers can not only validate the system's properties in a more detailed manner (than they might through empirical testing) but also use mathematical evidence as a compliment to system testing to ensure the correct behavior by constructing a mathematically robust model of a complex system. Formal approaches have a number of benefits, including the ability to remove/overcome the uncertainties of system requirements and state the underlying assumptions. They also reveal the errors/defects in system specifications, and their diligence allows a more detailed understanding of the problem. The model will address the dynamic automating and efficient fault identification of the distribution management system. The supervisory control and data acquisition system is the standard method for the communication between the components of the distribution network; it will be used for collecting the system faults through its communication facility. Non-deterministic finite automata are used for automating the failure detection and recovery procedures. Unified Modeling Language (UML) diagrams are used for the representations of the actors and their actions in the system, and they show how the components interact with each other. Formal methods in terms of the Vienna Development Method-Specification Language (VDM-SL) are used for the description and formal modeling of the system in a systematic way. Formal methods are mathematically based techniques supported by many tools that offer careful and effective ways to model, design, and analyze systems of the real world. Ambiguities and contradictions are often discovered while formalizing the informal requirements.