"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:
. 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.
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.
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.
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)