# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
**faultDetection**(voltsensorIn : Voltsensor) faultalert: bool

ext rd voltsensors : set of Voltsensor

pre voltsensorIn in set voltsensors

post faultalert <=> voltsensorIn.volt > voltsensorIn.nvolt and

voltsensorInfaulting=Transmitted>;

**Pre-conditions** (1) The pre-condition will check the fact that the voltage measuring sensor is in the collection of Voltsensor. **Post-conditions** (1) Fault alert will return true only if the volt value is greater than the normal volt that is nvolt; the fault info is transmitted to the control center. The major task of the distribution management system is to categorize the type of fault. Our operation determines that the fault type is quite lengthy yet easy to understand. The operation takes three transmission lines as input and the detector. The specified fields for fault detection in transmission lines are three transmission lines and one detector mounted on the tower. Read and write access is given to the collection of transmission lines, detectors, and the set of interrupted lines. **determineFaultType** (lineIn1 : Transmissionline, lineIn2 : Transmissionline, lineIn3 : Transmissionline, detectorIn : Detector) signal : Signal

**ext rd transmissionlines** : set of Transmissionline

rd detectors : set of Detector

wr tinterrupted : set of Transmissionline

**pre** lineIn1 in set transmissionlines and lineIn2 in set transmissionlines and lineIn3 in set transmissionlines and detectorIn set detectors and detectorIn.status=CON> and

tinterrupted = []

**post** if lineIn1.phasevoltage > 160 and lineIn2.phasevoltage > 160 then tinterrupted

<|and detectorIn.ftype = <Permanent> and detectorIn.fcat= <LL> and signal =

<OPEN_Recloser>

elseif lineIn2.phasevoltage > 160 and lineIn3.phasevoltage > 160 then interrupted

<|and detectorIn.ftype = <Permanent> and detectorIn.fcat= <LL> and signal =

<OPEN_Recloser>

elseif lineIn3.phasevoltage > 160 and lineIn3.zerocurrent > 35 then interrupted <|and

detectorIn.ftype = <Permanent> and detectorIn.fcat= <LG> and signal =

<OPEN_Recloser>

elseif lineIn2.phasevoltage > 160 and lineIn2.zerocurrent > 35 then interrupted <|and

<OPEN_Recloser>

elseif lineIn3.phasevoltage > 160 and lineIn3.zerocurrent > 35 then tinterrupted <|and

detectorIn.ftype = <Permanent> and detectorIn.fcat= <LG> and signal =

<OPEN_Recloser>

elseif lineIn3.phasevoltage > 160 and lineIn3.zerocurrent > 35 then tinterrupted <|and

detectorIn.ftype = <Permanent> and detectorIn.fcat= <LG> and signal =

<OPEN_Recloser>

else signal =<DO_Nothing>;

**Pre-conditions** (1) The pre-condition will check the fact that the transmission lines are in the set of transmission lines. (2) The status of the detector is working. (3) Initially, there is no pending fault such that the set of interrupted transmission lines is empty. **Post-conditions** (1) Two types of faults are detected in the post-condition by comparing the combinations of transmission lines. (2) Two constraints, phase voltage and zero sequence current, are used here for checking the proper working condition of the lines. (3) For any combination of two adjacent wires, if these constraints exceed the threshold value, the fault will occur and will be detected by the detector, which will determine the fault type as permanent and send a signal to the nearest recloser to open itself. (4) When two adjacent wires exceed the value of phase voltage, they will touch each other and the occurring fault will be a line-to-line fault. (5) If one of the three wires exceeds the phase voltage as well as the zero sequence current value, the occurring fault will be considered a line-to-ground fault. The following function takes the transformer ID as input and will send a signal to the control center about the restoration of the supply. In the post-condition, the mode is checked for that specific transformer if the result is true; if it is in the condition, then a restored signal is sent to the system; in the opposite case, it sends a signal to do nothing.