# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
**getDetails**(idIn: SBID) detailsOut : Details

ext rd substations : map SBID to Substation

pre idIn set dom substations

post detailsOut = (substations(idIn)).details;

**Pre-conditions** 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-conditionsThe mapping of the substations is applied on the entered ID of the substation, which will create an object, and, with the dot operator, it will take the value of the specified entry and return the appropriate fields of details for that particular substation. When the demand for electricity usage increases, the need will be to receive more power from generation resources so that the demand of the consumers is met. The extra received electricity needs to be stored in the main substation, which means the need will arise for new substation transformers of heavy capacity. The add transformer SB refers to the newly added transformer in the substation. The required fields for the new record are: the substation ID in which it is being deployed and recorded, transformer ID, capacity of the new transformer, its location, and the date on which the transformer was added into the system. The external clause is used to give the write access to the mapping of substations. addTransformerSB (idIn : SBID, idIn : TID, tcapacityIn : real, locationIn:String, dateIn:Date) ext wr substations : map SBID to substation pre idIn not in set dom substations post let trans = (substations-(idIn)).transformers in let newTrans = mk_Transformer(tidIn, <idle>, locationIn, tcapacityIn, dateIn) in substations = substations- ++ [idIn 1-> mu (substations- (idIn), transformers |-> trans union [newTrans])];

Pre-conditions(1) The registration of the specific substation is the first check by the system that the given ID is not in the mapping of the substation in which the transformer is added. Post-conditions(1) The let-in clause is used here to overcome the complexity of the operation. More than one let-in clause can be used in a single operation, such as in the post-condition. (2) Here, two local names 'trans' and 'newTrans' are used for the sub-expressions (substations-(idIn)).transformers and mk_Transformer (tidIn, <idle>, locationIn, tcapacityIn, dateIn), respectively. (3) Both of these local names are joined in the last sub-expression, with the union operation to add a new record in the substations mapping. The following operations are defined for the entity transformer. The add transformer operation is for the new transformer that is being deployed into the distribution network for the electric supply to the user. The required fields are the ID, location, and date of entry. addTransformer(tidIn:TID, locationIn:String, dateIn:Date) ext wr transformers : map TID to Transformer pre tidIn not in set dom transformers post transformers = transformers- - munion [tidIn 1-> mk_Transformer(tidIn, <idle>, locationIn, 33, dateIn)];

Pre-conditions(1) The pre-condition is to first check the transformers mapping to ensure that there is no already existing transformer with the same ID. Post-conditions(1) The post-condition accepts the ID of a new transformer and records the fact that this transformer has been added with the specified fields to the collection of transformers. The operation removeTransformer is similar to the addTransformer operation in nature except the fact that its pre-condition is different; it accepts the ID of a transformer and records the removal of this transformer from the system. removeTransformer(tidIn:TID) ext wr transformers : map TID to Transformer pre transformers <> {-|->} and idIn in set dom transformers and transformers(tidIn).mode <working> post transformers = (tidIn) < transformers-;

Pre-conditions(1) The pre-condition is to first check the transformers mapping to ensure that the accessed mapping is not empty; in brief context, in order to remove a record from the system, there should a record present in it. (2) The specified ID to be removed is in the collection of transformers.