# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
The aspiration of using formal methods in smart grids is to design a formalized model in an efficient way so that there is less chance of errors during the implementation because smart grids are a safety-critical domain, where a minor error can lead to severe destruction to equipment or serious harm to humans. An IoT-based automated distribution management system is introduced in the form of formal specifications. The system helps to ensure the correct and cost-effective functioning of the system at the user end as well as service-provider end because the designed system has been produced for substation automation; transmission line fault detection and its restoration; components management, such as transformers; and the specifications of smart meters, enabling the properties of advanced metering infrastructure. The absolute necessity of employing formal techniques in safety-critical systems leads to the suggested system's precision, consistency, and correctness. To demonstrate and justify the formal specification's validity, the Vienna Development Method-Specification Language (VDM-SL) was deployed. The formulated specification of the IoT-based formal model of a distribution management system was then substantiated and analyzed by employing the VDM-SL toolbox facilities. The reported errors were eliminated earlier by enhancing the characteristics of invariants and pre/post-conditions. Moreover, examining specifications \begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Specifications** & **Syntax Check** & **Type Check** & **Integrity Check** & **C++** & **Pretty Printer** \\ \hline checkCapacity & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ getDetails & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ addTransformer & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ removeTransformer & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ toRepair & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ fixedTransformer & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ numberToFix & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ getTotalTransformer & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ detectTransformerTheft & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Formal analysis of the transformer module. \begin{table}
\begin{tabular}{c c c c c c} \hline \hline
**Specifications** & **Syntax Check** & **Type Check** & **Integrity Check** & **C++** & **Pretty Printer** \\ \hline faultDetection & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ determineFaultType & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ serviceRestore & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ isFaultyLine & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ removeFaultyLine & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ lineRestore & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ tripCB & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ isVoltDetected & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ checkCapacity & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ getDetails & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ requestMeter & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ installMeter & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ loadLimit & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ removeMeter & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) & \(\surd\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Formal analysis of the fault detection module. and implementing them by utilizing comprehensive computer tools enhances reliability through the exploration of possible problems in the initial phases of the development of system design. We would like to point out here that the framework recently proposed here presents only a few distribution level components.