# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model  
Formal methods are mathematical entities that are used to model complicated systems. It is feasible to validate the characteristics of a complex system in a more formalized manner than empirical testing by developing a mathematically rigorous model of the system. Formal specifications are the descriptions of a model that can be described in a thorough and consistent manner for an application domain, a requirement or a group of requirements, software architecture, or program organization [41]. The proposed model in this article signifies yet another contribution in this field. In programming languages, composite types are equivalent to record types. The static components include invariants for integrity checking of the condition, which must always hold true, and the fields, in the case of composite objects, may have several data types. In the formal specifications  
Figure 7: UML sequence diagram of fault detection in a substation. of the distribution system, one portion includes the data types of the variables, alongside which their quote types are declared. The model is comprised of various variables such as sequence type, token type, and string type. To record everything in the system, the date and time are taken as composite objects. ``` TypesLID=token; DID=token; SID=token; SBID=token; TID=token; Details=token; Wire=token; String=seq of char; CName=String; CID=token; MID=token; Relay=token; Ack=\(\text{<}\text{yes}\text{<}\text{no}\text{>}\); Mode=\(\text{<}\text{idle}\text{>}\)\(\text{|}\)\(\text{<}\text{working}\text{>}\)\(\text{|}\)\(\text{<}\text{damage}\text \begin{tabular}{l} Transmission line : lineid : LID \\ detector : Detector \\ phasevoltage : real \\ zeroscurrent: real \\ line1 : Wire \\ line2 : Wire \\ line3 : Wire \\ inv.mk_Transmissionline(\(\sim\)11,12,13) == (11\(\div\)12 and 11\(\div\)13 and 12 \(\div\)13); \\ \end{tabular} 

The detector is the one that is embedded in each transmission line and the near-to-field devices, such as transformers and meters, and in the substation area. Each detector is distinguished based on the unique ID. The possible values of the detector status would be on and off. The purpose of the detector is to determine the type of the fault, whether it is temporary or permanent, and if the fault is permanent, it will further inform about the category of the fault, whether it is \(<\)LL\(>\) line-to-line fault, \(<\)LG\(>\) line-to-ground fault, \(<\)LLG\(>\) double line-to-ground fault, or \(<\)LLL\(>\) line-line-line fault. To keep the database of faults updated, it is necessary to add the date and time of the fault. \begin{tabular}{l} Detector := id : DID \\ status : Status \\ type: Flype \\ fact:Fcat \\ signal : Signal \\ fdate : Date \\ \end{tabular} 

The composite object Voltsensor is created for the sensor, which is used for measuring the voltage of the power. The deviation in the nominal values of voltage and current causes most electrical faults, so it is most important to continuously measure the value of the voltage in the lines. Actual load and requested load are those values of the voltage that are actually flowing and demanding, respectively. The sensor will send the alert message to the control center and provide the fault info. \begin{tabular}{l} Voltsensor : \\ voltreal \\ nvoltreal \\ actuaload : int \\ requestedload : int \\ fault alert: FAlert \\ faultinfo: FInfo: \\ \end{tabular} 

The keyword **values** is used to specify the constants of the specifications in VDM-SL. This declaration of values comes right before the state definition. Here, we declare the phase voltage and zero sequence current values. These values will be used in the fault detection operation. These values are specified here for the efficient working of the system. If the threshold values are exceeded, the system will go into the imbalance condition, which is the faulty state. \begin{tabular}{l} \hline
**Values** \\ phasevoltage = 160; \\ zeroscurrent = 35; \\ Limit = 200; \\ \end{tabular}