# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 2 Related Work  
The identification of the faulty line section is made possible with the petri net theory. The data concentrator units transfer and receive the fault signal, including the pre/post-fault current of the lines. The measurements of the feeder loading and statuses of the fault indicators play an important role in the petri-net-based fault identification method. The measurement of the feeder loadings and the pre/post-fault current values are compared to find out the loading mismatch of the feeder. The wireless LoRa module is used for all the communication between the equipment, feeder devices, and the web server [5]. An IoT-assisted power monitoring system using ThingSpeak technology is proposed in this paper. It provides an easy method for consumers and service provider companies to monitor and analyze the electrical parameters of the load data at the remote end. The arrangements are prepared with the integration of WiFi-based nodes, Arduino UNO, and an LCD for local display. WiFi nodes fetch the consumer's load voltage and values of current sensors, and the Arduino interacts with the sensors to collect load information. The WiFi module works as an intermediary gateway between the monitoring panel and the webserver; it transfers the real-time data to Thing5 peak for storage and manipulations [6]. The model checking framework is proposed with the intent of strong and resilient smart grid practices in accordance with distributed intelligence. In one study, the author auto-developed the formal model for two distributed grid intelligence systems in a symbolic model-checking language, and the proposed model was verified with the NuSMV model checker. Tests were created for model-checking the computational tree logic properties, and the initial obtained results were satisfactory [7]. A innovative prototype scheme was developed for the distribution SCADA system. The proposed scheme was developed by using smart meters for the automation of the distribution network. The smart meter would be installed at the substation for tracking the demand/supply parameters, the detection and location of faults, and bidirectional communication using GSM technology. With the integration of microcontrollers and GSM, the scheme identifies the fault type and its location, and there is an indication on the consumer's mobile [8]. To the best knowledge of the author, Ref. [9] is the first article on modeling a smart grid framework based on formal specifications using Z-language. Though the author does not work on the deep level infrastructure of the smart grid components, as titled, the study presents brief specifications on domains such as smart appliances, wind turbine systems, solar systems, and storage with limited conditions. An overall networking-based scheme for smart grids is presented in [10], from the integration of a wireless sensor network to its routing protocol and from possible attacks to its countermeasures, but the author remains precise on these topics and does not provide much research on the security protocols of smart grid communication. The faults of distribution systems are diagnosed using a programmable logic controller and supervisory control and data acquisition system in [11]. The programmable logic controller is used for analyzing the different parameters of transformers, such as oil levels, voltages, and the load current and its temperature. The suggested monitoring procedure works with the integration of solid-state plc devices and the package of sensors. The proposed scheme provides the facility to detect the internal/external faults of transformers, and whenever a fault occurs in a three-phase line, the detection circuit indicates the abnormal condition. Visual representations are shown in the system, which helps the crew to clear the faults and reduce the patrolling time.