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

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.

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, r_g 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. R_g, associated with the receive action, updates internal desired power generation according to a message sent by the power controller. In the transmit action, t_g is a constant function that returns a channel for communicating generator output, and T_g updates the time of the last feedback message.
. In the consumer's looped transmit action, c_f outputs a constant channel used for consumer feedback. C_o, as T_g, simply updates the time of the last sent message. The transmit action that jumps an element to the "graveyard" uses t_gr 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 t_g and updates its internal expected generator output with G_i. C_i works the same way for consumer feedback. G_o and g_o 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, C_d 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.