A smart grid is an energy network where users (like households) may consume or produce energy. This example is taken from Biondi et al.
The users periodically negotiate with a central aggregator in charge
of balancing the total consumption among several users. In practice each user
declares to the aggregator its consumption plan. The aggregator sums up
the consumptions of the users and checks if it falls within admitted bounds.
If not it answers to the users that the consumption is too low or too high by a certain amount, such that they adapt their demand.
This model raises some privacy issues as some attacker can try to guess the consumption of a user, and for instance infer whether or not this particular user is at home. The input code for the example is as follows:
const N:=3; // N is the total number of users
const S:=1; // S is the number of users we care about
const C:=3; // C is the possible consumptions level
const M:=0; // M is the consumption level of the attacker
const LOWT:=2; // LOWT #\textrm{is the lower threshold
const HIGHT:=9; // HIGHT is the upper treshold
// the observable is the order given by the control system
observable int32 order;
observable int1 ordersign;
// The secret is the consumption of each user we care about
secret array [S] of int32 secretconsumption:=[0,C-1];
// The other consumptions are just private
private array [N-(S+1)] of int32 privateconsumption:=[0,C-1];
public int32 total:=M; // this is the projected consumption
public int32 j:=0; // this is just a counter
// count the secret consumptions
for (i in [0,S-1]) do
while (j<C) do
if (secretconsumption[i]==j) then
assign total:=total+j;
fi
assign j:=j+1;
od
assign j:=0;
od
// count the private consumptions
assign i := 0;
assign j := 0;
while (i<N-(S+1)) do
while (j<C) do
if (privateconsumption[i]==j) then
assign total:=total+j;
fi
assign j:=j+1;
od
assign j:=0;
assign i:=i+1;
od
if (total<LOWT) then
assign order := LOWT - total;
assign ordersign := 0;
elif (total > HIGHT) then
assign order := total - HIGHT;
assign ordersign := 1;
else
assign order := 0;
assign ordersign := 0;
fi
return;
In the following figures we present the experiment results of this smart grid example for different numbers of users. HyLeak takes less time than both fully precise analysis and fully randomized analysis (as shown in the first figure).
Moreover it is closer to the true value than fully randomized analysis
especially when the number of users is larger (as shown in the second figure).
