# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
(3) The working mode of the transformer is checked, in that its status should not be working, which means its status can be any other than working. **Post-conditions** (1) The post-condition accepts the ID of a new transformer and removes the required transformer from the collection of transformers. To record a transformer as damaged, the operation to repair accepts the ID of a transformer and records its mode as damaged. To change the records of the composite object, the write access is given to the transformers mapping with the external clause. **toRepair(tidIn:TID)**

ext wr transformers : map TID to Transformer

pre tidIn in set dom transformers

post transformers = transformers- ++ {tidIn!-> mu(transformers-(tidIn), mode!-> <damage));

**Pre-conditions** (1) The pre-condition is to first check the transformers mapping to ensure that the transformer is in the collection of transformers. **Post-conditions** (1) The post-condition accepts the ID of the transformer, and, by using the override, the operator changes the required fields of that transformer, and then the collection of transformers will be updated. To update the record of the transformer's collection, the operation fixedTransformer accepts the name of a damaged transformer and records that its mode is set to idle; the other process is the same as above. **fixedTransformer(tidIn:TID)**

ext wr transformers : map TID to Transformer

pre tidIn set dom transformers

post transformers = transformers- ++ {tidIn!-> mu(transformers-(tidIn), mode!-> <idle)};

The operation numberToFix returns the number of total damaged transformers. The operation will return a natural number value. **numberToFix0 out: nat**

ext wr transformers : map TID to Transformer

**pre true**

**post out = card {t! t in set mg transformers & tmode = <damage);**

**Pre-conditions** (1) The pre-condition is true here, which refers to the condition that there is no need to apply any check or constraints because, without any pre-condition, the post-condition will work perfectly, such that it is just a read type operation. **Post-conditions** (1) The cardinality operator is used here to take the number from a set type. (2) The condition in braces checks that there exists a transformer in the range of the transformers mapping of them; if the mode is damaged, then the total gathered transformers will be returned as a number. To determine the total number of transformers under a substation, we created the operation of get_total_Transformer, which will return a natural number value. **get_total_Transformer()**

ext rd substations : map SBID to Substation

pre true

post out = card dom substations;

The important aspect of the distribution management system is to detect the theft of equipment in the substation. It can be ensured by checking the supply or working mode of the transformer; the operation will take the ID of the transformer as input and the query will return as true or false, depending on the post-condition check. **detectTransformerTheft(tidIn:TID)**

ext wr transformers : map TID to Transformer

**pre true**

post query <-> tidIn in set dom transformers and transformers(tidIn).mode <- <working>;

**Post-conditions** (1) The query will return as true when the specified transformer is in the record of the substation but the system shows its mode is not working. (2) We ensure that we have already created an operation of damaged transformers, so it cannot be considered that if a transformer is not working, it is in the damaged transformer collection. (3) Thedamaged transformer records are updated with the time, so a nonworking transformer will be considered as lost. To detect the fault in the transmission line, a volt measuring sensor is taken as input in the following operation; it will return a Boolean type value in the form of true/false.