# Formal Modeling of IoT-Based Distribution Management System for Smart Grids
## 4 Formal Model
### Static Model
**serviceRestore(tidIn: TID)** signal: Signal

ext rd transformers: map TID to Transformer

pre tidIn in set dom transformers

post if transformers(tidIn).mode= <working> then signal = <Restored> else signal =

<ID> Nothing>;

**Pre-conditions** (1) The pre-condition is to first check whether the given ID is in the collection of transformers. **Post-conditions** (1) The specified transformer mode is checked as to whether it is working or not. If the mode is equal to working, then a signal will be transferred to the control center that the service has been restored. The following operations are specified for the transmission lines. For checking the specific line against an ID, the first operation is used, which will check that line in the interrupted collection of wires. After resolving the fault of the specific line, it will add up to the collection of transmission lines; _transmissionlines_- is the old set of transmission lines and transmissionlines is the updated collection. To remove a faulty line from the interrupted transmission line collection, write access is used here to change the record. Sometimes, the continuous flow of the current in the wires gets changed due to some inner or outer conditions of the system, and the system starts tripping; this tripping mostly happens in the nearest circuit breaker. **lineRestore(linedIn: LID)**

ext wr transmissionlines: set of Transmissionline

pre true

post transmissionlines = transmissionlines- union [lineidIn];

**removeFaultyLine()**

ext wr interrupted: set of Transmissionline

pre interrupted <> {}

post interrupted = |;

**tripCB**(voltsensorIn: Voltsensor) trip: bool

ext rd voltsensors: set of Voltsensor

pre true

post trip <=> voltsensorIn.requestedload > voltsensorIn.actualload;

The following are the smart meters' operations: initially, the consumers request that the smart meter be installed at their residence; the required attributes are taken as input, which is stored in the system for further use in the future. The smart meter installation takes the required data of the user as input and also the unique ID of the meter that is being installed. The last two operations are regarding the usage of the units and meter removal. **requestMeter(cidIn: CID),cnameIn: CName, datelIn: Date, detailsIn: Details)**

ext wr requesteds: map CID to **Consumer**

rd processesdusers: map CID to **Consumer**

pre cidIn not in set dom requestedusers

post requestedusers = requestedusers- munion [cidIn: ]>mk_Consumer(cidIn, cnameIn,

**dateln, detailIn);**

**Pre-conditions** (1) The pre-condition is to first check that the request has not already been registered against the ID of the consumer. **Post-conditions** (1) The post-condition is updating the mapping of the requested user. The installMeter operation will record the fact that the request of the specified consumer is completed with the complete details of the consumer and that the date of the record is also updated. **InstallMeter(cidIn: CID), cnameIn: CName, dateIn: Date, detailsIn: Details, midIn: MIDJack: Ack ext wr processesdusers: map CID to Consumer wr meters: map MID to Smeter rd requestedusers: map CID to Consumer**

pre cidIn in set dom requestedusers and midIn not in set dom meters post meters= meters- munion [midIn 1\(>\) mk_Smeter(midIn,2000)]

and processesdusers= processesdusers- munion (cidIn 1\(>\) mk_Consumer(cidIn, cnameIn, dateIn, detailsIn))andack=xyes;

**Pre-conditions** (1) The pre-condition is to first check that the request is not yet processed and the meter ID is not in the already installed meter collection. **Post-conditions** (1) The post-condition is updating the mapping of the meters; the requested user is added to the processed users, and an acknowledge message is sent to the system that a new meter has been installed and the request has been processed. To limit the usage of the electricity unit, the load limit operation is specified here, in which the pre-condition ensures that the meter is in the collection of meters and the usage limit is crossing or exceeding the specified value.