# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 3 Problem Statement and System Model  
Compared to the traditional grid, there are higher expectations with the smart grids to provide better services. Utility firms intend to convert the present unidirectional grid into a bi-directional power grid, with the goal of storing energy in the electrical system and using it wherever it is needed. Among other safety-critical applications, smart grids need precise modeling and the analysis of systems such as demand response, distribution automation, energy storage, and fault detection. These applications are critical because even a minor design flaw can have serious consequences, even at the expense of individual life and property. The present electricity grid is predicted to have expertise in the difficulties in the generation, transmission, and distribution of the requisite power for massive amounts of the demanding load. Considering the sophistication and complexity of today's distribution networks, there is always the risk of underlying errors in models that are not detectable by evaluating a small number of scenarios. Network failures and high operating expenses might occur if these models fail. As a result, it appears that a mathematical model for distribution automation capabilities in smart grids that can be confirmed is required. The aim of this paper is to design a systematic model for a distribution management system comprised of substations, feeders, and smart meters. Modeling an IoT-based automated distribution management system will portray equipment utilization in substations, fault detection, and a recovery mechanism in transmission lines for the integrity and efficiency of the system.  
\begin{table}
\begin{tabular}{c c c c c} \hline
**Reference** & **Year** & **Description** & **Limitation** & **Formal Modeling** \\ \hline \multirow{3}{*}{[9]} & \multirow{3}{*}{2018} & State based formal specification framework for smart grid generation components is presented in this paper. & The formal modeling has been designed only for the state identification of the smart grid components. & Yes \\ \hline \multirow{3}{*}{[35]} & \multirow{3}{*}{2017} & Formal modeling approach is used generically for smart transformers. & The given mechanism of theft detection and user communication is poor. & Yes \\ \hline \multirow{3}{*}{[30]} & \multirow{3}{*}{2020} & Distribution dispatching control system is discussed in this paper. & The standard petri nets are used, which have the distinct disadvantage of producing very large and unstructured specifications for the systems being modeled. & No \\ \hline \multirow{3}{*}{[36]} & \multirow{3}{*}{2019} & Decentralized service restoration strategy is applied & Unable to restore services where DGs are not available. Presented switching order is complex and occupies more time. & No \\ \hline \multirow{3}{*}{[37]} & \multirow{3}{*}{2018} & \multirow{3}{*}{2018} & The provided technique is expensive with regard to installing external components. Moreover, it cannot prevent PV inverter shutdown during the fault event. & No \\ \hline \end{tabular}
\end{table}
Table 1: Comparison between previous studies and the current study.