# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model


### Dynamic Model

The dynamic components include the state definition, the possible operations, and the reusable functions. Various constructs, such as composite objects, invariants, sets, and pre/post conditions, are used for developing the specifications. IoT is deployed in the smart grid for detecting the faults that consist of sensors and detectors. The exceptional part of the VDM-SL specification is **state,** in which the variables are declared in a similar manner as in the other programming languages. The attribute specified in the state is permanently stored by the system. The illustration/explanation of specifying the state for our DMS is as follows. Many variables have been declared, with their data types being used in the state. Invariants are defined in these variables, which must be true for the system from the beginning to the system termination. The state of the system is always finished with the keyword **end**. \begin{tabular}{l} \hline state **DMS** of \\ detectors : set of Detector \\ transformers : map TID to Transformer \\ transmissionlines : set of Transmissionline \\ vollsensors : set of Vollsensor \\ substations : map SBID to Substation \\ interrupted : set of Transmissionline \\ requestedesures : map CID to Consumer \\ processesdusers : map CID to Consumer \\ meters : map MID to Smeter \\ inv mk_DMS(-_t-,-,-,-,-) == forall n in set dom t \& n = t(n).tid \\ init dms == dms = mk_DMS([_l,[_l_|->],[_l_|,[_l_|->],[_l_|->],[_l_|->]) \\ \end{tabular}  ) \\ \hline \end{tabular}

The function is another tool that is vital when specifying complicated systems. These functions can be used later in operations. The following function is defined to check the voltage: nvolt is the normal voltage, and volt is the abrupt change in the voltage if it becomes high. We will use this function later in our operation of fault detection. **Functions**

**isVoltDetected**(volt : real, nvolt : real) faultalert: bool

pre true \\ post faultalert <=> volt > nvolt; \\ \end{tabular}

The dynamic behavior of the system is described by exploiting operations. A non-mandatory pre-condition and a mandatory post-condition are required to represent the operation. By specifying the pre-conditions, each operation is correlated to the preceding one. Post-conditions are used to specify the accuracy of an operation. Our proposed formal model performs various operations on the distribution management system, such as checking the capacity of the substation to get its details and adding transformers to the substation. _Operations_

The operation check capacity is designed to measure the total capacity of any specific substation in the smart grid. The capacity refers to the capability of power storage and power transfer to the distribution transformers. It takes one input, which is the ID of the specific substation, and will return the value of the capacity in the real data type. Before proceeding to the post-condition, the system will ensure the pre-condition. In the external clause, the rd keyword is used to tell the system that the access type is only to read. **checkCapacity**(idIn: SBID) cap : real

ext rd substations : map SBID to Substation

pre idIn set dom substations

postcap = (substations(idIn)).capacity;

**Pre-conditions** (1) The registration of the specific substation is the first check by the system that the given ID is in the mapping of the substation in the system record. **Post-conditions** (1) The mapping of the substations is applied to the entered ID of the substation, which will create an object; the dot operator is used with the capacity attribute, which will take the value of the specified entry and return it as a real number. The get details operation is defined for getting the details of the specific substation. This operation is useful for obtaining the overall detail of the substation at any time; the system is updated periodically.