# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
In the post-condition, the status of the meter load limit will be enabled. **loadLimit(midIn: MID)**

ext wr meters: map MID to Smeter pre midIn in set dom meters and meters(midIn).munits>Limit

post meters = meters- ++{midIn 1\(>\) mu (meters-(midIn), status 1\(>\) <Enable>)};

The removeMeter operation illustrates the procedure of removing a meter that has crossed the limit of the given units and has not yet paid for the previous transaction. **removeMeter(midIn: MID)**

ext wr meters: map MID to Smeter

pre midIn in set dom meters and meters(midIn).munits>Limit

post meters = {midIn} \(\ll\): meters- ;

## 5 Model Analysis

To analyze and verify formal specifications, the VDM-SL toolbox was deployed through the exploitation of its prevailing service. The toolbox comprises various services for ensuring accuracy, such as syntax and type checking, pretty printer, C++ code generation, interpreter, integrity inspector, dynamic verification, and several other validations and analysis techniques. No tool exists to provide a complete guarantee of the absolute correctness of any system model. Therefore, the formal specification does not assure that system is completely accurate. However, it helps in the identification of the possible errors at the initial stages of any software development. The design and analysis of the model help to recognize areas of ambiguity and incompleteness in the requirements of the informal framework and give a degree of assurance that the key properties, in particular those of safety or security, will be appropriate for legitimate implementation. The specifications of the system are analyzed through the VDM-SL toolbox. The specification is evaluated via syntax, type checker, generator of C++ code, and pretty printer. In the formal specification, the reported errors are eliminated earlier by enhancing the characteristics of invariants and pre/post-conditions as well. The developed formal specification is approved with success through all checkers, and the proof of correctness is shown in Figure 8.

An integrity analyzer is used to determine the specification's integrity properties. The dynamic level of the requirements is examined by the integrity checker, and VDM-SL predicates are defined by a set of formulated integrity properties that specify the parameters in which no runtime error should execute. There will be no runtime error if the integrity property responds to true. All integrity properties are found to verify the true condition of the specification. For the validation of model properties, invariants and pre/post-conditions are specified. There are two functions that are necessary to be performed in order to ensure the system's formal validation's validity. The VDM-SL toolbox provides syntax and type checkers that evaluate the developed static and dynamic models. Initially, there were numerous syntax and type errors within the model specification, which were explored by the tool's syntax and semantics evaluation as shown in Figure 9.

The detailed description of the proposed model is defined in tabular form, as given in Tables 2 and 3. Figure 8: Proof of correctness. Figure 9: Model analysis. ## 6 Conclusions

The smart grid is an excellent innovation of engineering and technology for the modern world. There are numerous studies concerning the distribution layer of the smart grid, but this is majorly concentrated on the modeling of the distribution management system because very little work has been done in this domain. The obligation is to utilize the current state-of-the-art technologies in better sensing, detecting, communicating, and controlling the grid, especially the distribution network layer, to make the grid robust, efficient, and resilient. In this article, we present the formal model of an automated distribution management system for smart grids.