Simplified Smart Grid
A Case Study

A more verbose description of the model can be found in a tech report.

> Description_

"A Smart Grid is a form of electricity network using digital technology. A smart grid delivers electricity from suppliers to consumers using two-way digital communications to control appliances at consumers' homes; this could save energy, reduce costs and increase reliability and transparency if the risks inherent in executing massive information technology projects are avoided. The "Smart Grid" is envisioned to overlay the ordinary electrical grid with an information and net metering system, that includes smart meters. Smart grids are being promoted by many governments as a way of addressing energy independence, global warming and emergency resilience issues."

Source: Wikipedia
 
> Model Description_

In this case study, we implement a simplified Smart Grid scenario in the Distributed Probabilistic-Control Hybrid Automata framework. Our objective is to establish a basic working Smart Grid infrastructure and then check its behaviour using Statistical Model Checking by verifying interesting properties specified in Quantified Bounded Linear Temporal Logic. We obtain traces of 24h duration in this case study, each representing one day's consumption. The model consists of 4 types of entities:
. Consumer: this type of entity generates power demand that varies according to the time of day and its own lifecycle. It is an abstract representation for sets of appliances that are turned on at roughly the same time for roughly the same duration. To more accurately represent daily consumption of energy, several elements of this type can exist at the same time, and the overall demand is nothing more than the sum of their demands. Depending on the type of day at which consumers are created in the system, they can behave in one of two ways: high-consumption short-span or low-consumption long-span, an illustration for which can be found below.


. Power Generators are the producers of energy. The Smart Grid must dynamically match the output of generators to the demand of the consumers. Generators can have different properties, mostly related to how fast they adapt power output (e.g. maximum values of its first and second derivatives). Our current model consists of a single, high-output generator.
. The Power Controller (PC) is the Smart Grid's nerve centre. It maintains up to date information about consumer demand and generator output. It is in charge of adapting each generator's output to match demand. Periodically, it applies a policy for changing a generator's requested output to match power and demand.
. The Consumer Controller (CC) is responsible for creating and keeping track of the consumers in the system. It represents the probabilistic environment. Each trace of the CC and its consumers contains energy consumption over the duration of one day. We have a bound of 20 on the number of consumers, and they are spawned with a different probability depending on the time of day. At an interval given by a Normal random variable of 5 minute mean and 1m variance, the CC decides whether to receive messages or spawn another consumer. The probability distribution over these choices changes according to the time of day. If there is a message indicated a consumer has left the system, it is received and the state updated accordingly. Otherwise, the probability of spawning a new element is given by the following table.
 
12345678910 11121314151617181920 21222324
0.200.050.070.100.100.200.100.200.100.20 0.100.200.100.200.200.100.000.000.000.00 0.000.000.000.00

High-demand consumers are spawned between 4am to 12pm, and low-demand but long-span for the rest of the day. We thus model high consumption throughout the day and lower consumption during the evening and night. Two examples of daily consumption generated by the current model can be found in the following graphs.

> Automaton_

It is very hard to graphically represent DPCHA. An incomplete representation can be found below. We say it is incomplete because we do not show each element's state, nor do we show the transition probabilities for more than one element in each position (although there can be multiple elements at the same position, as the number of dots in each location node show).

Zero probability in receive action edges simply means that no messages are available, or that other edges, for one reason or another, are more important. For instance, more important messages may be received first.

. In the generator component of the automaton, rg outputs a reusable channel based on the generator's ID (which is part of its state), through which messages directed at it can be received. Rg, associated with the receive action, updates internal desired power generation according to a message sent by the power controller. In the transmit action, tg is a constant function that returns a channel for communicating generator output, and Tg updates the time of the last feedback message.
. In the consumer's looped transmit action, cf outputs a constant channel used for consumer feedback. Co, as Tg, simply updates the time of the last sent message. The transmit action that jumps an element to the "graveyard" uses tgr to get a channel for communicating the exit of a consumer element. In this case, I is the identity function, i.e. it has no effect on state. Once at the graveyard, the consumer immediately exits the system.
. The power controller receives generator output feedback messages through tg and updates its internal expected generator output with Gi. Ci works the same way for consumer feedback. Go and go use a policy for deciding to change the output of which generator (in our case, just one), and by how much. Internal state is changed to reflect the desired changes.
. The consumer controller maintains up to date information about which consumers exist. In particular, Cd changes the internal state of the CC to indicate that the consumer source of the message has exited the system. The CC is also in charge of creating consumers with the edge annotated with a new action. N is the function that decides the new element's state. Its location will always be the consumer location, but the state and evolution depend, as seen previously, on the time of day.

Messages sent over feedback channels that are used by several elements in the system generally contain an element's ID. This ID never changes over time. This allows the receiving element's state to be updated according to this ID. The PC, for instance, maintains information about all the generators and all the consumers stored in its state space, changing information using the indices received in messages.

> Files and Dependencies_
. SmartGrid.java (java)
. DPCHA Framework (link)
 
> Links_
< Main Page DPCHA Framework >