Smart grids

A smart grid is an electric grid or network that enables the management of smart devices based on data gathered from the network to react quickly to demands for electricity. It allows to enhance the electric network in reliability, availability, and efficiency.

The smart grid can be categorized by levels such as the customer, the distribution system, and the transmission system during operation. At the customer level, it may involve some things like meters that can be read automatically, meters that communicate to customers, control of customers’ loads, and flexibility in the use of time-of-day or time-of-use meters. At the distribution level, system may involve distribution system automation, selective load control, managing distributed gen- eration, and ”islanding”. And the transmission level, system may involve measurement of phase and other advanced mea- surements, and other advanced control devices, distributed and autonomous control 18.

The main objectives of designing smart grids are to achieve grid visibility, enable asset control, improve power system performance and security, and lower the expenses of operation, maintenance, and system planning. In the research of smart grid, there are some computational tools for modeling and analysis of the smart grid20, 21, 22, 23, 24, 25, as well as studies on threats and solutions26.

Formal verification

Formal verification is a research direction aimed to prove the correctness of a system with respect to a certain property rep- resented in a formal specification. Theoretically, verification is a process of finding formal proof on a formal/mathematical model of the system under test. There are two main ap- proaches in formal verification: model checking and theorem proving3.

In model checking, a finite model of a system is used for searching for evidence of a violation of the desired property. The system is verified when no such violation evidence exists or a counter-example will be shown. It is a very practical approach, even though in the explosion of the state space, the search (for violation) can stop within a limit of computer resources and running time and returns the correctness with some confidence level 27. The well-known logic used in model checking is temporal logic, which aims to capture the temporal aspect of the property. For example, one can check if a smart grid satisfies the property “Definitely, the top priority consumer will receive enough energy as required”. Although, in theory, the search in the state space is exhaustive, there are researches in the model checking field to overcome this drawback9, 15, 16, 17, 28.

In theorem proving, both the system and its desired prop- erties are expressed as formulas in some mathematical logic, which is based on axioms and inference rules. By that logic, it can deal directly with infinite state space, while model checking can hardly. However, some of the theorem techniques are used in practice with excellent results28.

Colored Petri Nets

A Petri net is a system model that uses a weighted, directed graph of nodes as places and transitions. Directed arcs connect places to transitions (as inputs) and transitions to places (as outputs). The Petri networks by moving tokens from (input) places to transitions and from transitions to (output) places (firing). The weight of the directed arcs determines the number of tokens moved (transmitted).

Colored Petri net (CPN)14 is an extension of Petri net that merges the benefits of Petri nets with the expressive power of functional programming languages by giving more features and properties to tokens, places, and transitions resulting in more classes of high level. It enables tokens to have a data value attached to them called the token color, and each place represents a color set. Furthermore, arc-expressions (an extended version of arc weights in classical Petri nets) determine which tokens can flow over the arcs. Additional guard constraints on enabling transitions can also be expressed as Boolean expressions.

A Colored Petri net is a tuple CPN= (ColBagPlaTrnV arFun), where

• Col define a finite set of color sets.

• Bag is a bag of tokens (value) of colors c ∈ Col.

• Pladefine a finite set of places.

• Trnis a finite set of transitions.

• V ar is a finite set of variables v ∈ V ar.

• Fun define a finite set of functions.

For example, Figure 1 shows a CPN in its two stages: enabling and firing. In Figure 1(a), place P 1 consists of 2 bags of integer tokens (one with five (5) tokens and another with three (3) tokens), and place P 2 contains a bag of four (4) integer tokens. They are the input places for transition T 1 with the guard expression x > y (from P 1 and P 2, respectively) as the condition to enable the transition. In Figure 1(b), the transition T 1 has been fired when the guard expression is confirmed (the bag of 5 tokens in P 1 and the bag of 4 tokens in P 2). It removed those tokens from place P 1 and P 2 and produced tokens in P 3 (a bag with 14 integer tokens as the outcome of the output arc-expression 2x + y).

Smart grid representation using Color Petri nets

Based on characteristics of a smart grid, we proposed that the grid can be represented using two generic components: generation and transmission/ consumption. Each of these com- ponents is modeled by a CPN.

An illustration of those representations is in Figure 3. Figure 3(a) is a pure petri net created from the topology in Figure 2 by reducing the busses and CBs. The left part of the petri net describes the power generation with three Generators G1, G2, and G3. From these three generators, power is generated through transitions gen1, gen2, and gen3 and is stored in the place “Generated”. After being generated, power will be transferred and consumed in place “Consumer C1”, “Con- sumer C2” and “Consumer C3” through transitions trans1, trans2 and trans3, respectively.

To use the power of the Color Petri net for making a simpler net, all generators and consumers are merged into the places Generator and Consumer, respectively, as displayed in Figure 3(b). All generators (gen1, gen2, gen3) and transi- tions(trans1, trans2, trans3) have also been folded to functions fn_gen, fn_trans, and fn_cons as in Listing 3 to describe power generation, transmission, and consumption, respectively.

Figure 4 and Figure 6 show the details of two folded compo- nents, which will be explained in more detail later.

The declarations are presented using the Coloured Petri Net- Modelling Language (CPN-ML) syntax of the CPN Tool9 as follows (see Listing 1).

Color set types:

• “IDX”: integer, a unique id of a node in the grid.

• “TYPE”: enumeration = [GEN,CON] for Genera- tor and Consumer (Load).

• “CAPACITY”: integer, the capacity of a generator or consuming capacity of a consumer.

• “NODE”: a record of IDX * TYPE * CAPACITY, a node in the grid.

• “POWER”: an amount of power.

• “NODE_POWER”: a product of “NODE” and “POWER”, for power generated or consumed by the NODE.

The configuration of the grid described in Table 2 is in Listing 2. It is also called the initial marking of the CPN. Listing 2 shows the initial marking of the “Generator”, “Generated” and “Consumer” place. Generators are initialized with full energy production capacity. Generated place contains zero power at the initial stage.

Listing 3 describes three functions for power generation, power transmission, and power consumption. How these func- tions work is described in section below.

Listing 1

Declarations of the color sets.

1. c o l s e t IDX = i n t

2. c o l s e t TYPE =

3. c o l s e t CAPACITY = i n t

4. c o l s e t POWER = i n t ; 5

5. c o l s e t NODE = r e c o r d i : IDX* t : TYPE* c : CAPACITY

6. c o l s e t NODE POWER = p r o d u c t NODE*POWER;

Listing 2

Initial marking of the place “Generator” and place “Consumer”.

8 v a l i n i t G e n e r a t o r : NODE POWER =

9 [ ( { i = 1 , t = GEN, c = 10 } , 10 )

10 , ( { i = 2 , t = GEN, c = 5 } , 5 )

11 , ( { i = 3 , t = GEN, c = 6 } , 6 ) ]

12 ;

13 v a l i n i t C o n s u m e r : NODE POWER =

14 [ ( { i = 4 , t = CON, c = 6 } , 0 )

15 , ( { i = 5 , t = CON, c = 9 } , 0 )

16 , ( { i = 6 , t = CON, c = 6 } , 0 ) ]

17 ;

18 v a l i n i t G e n e r a t e d : POWER = 1 ‘ 0

Smart grid component representation

We provide more details about the components mentioned above in this section. The generation component has a tran- sition “gen” and two places “Generators”, “Powers”. The Generators place holds all generators of the smart grid.

For example, the Generator place in Figure 4 contains three generators G1, G2, and G3 of the smart grid in Figure 2, with the configuration as in Table 2. The Generator G1 (ID: 1, maximum power generation capacity: 10) is setup to generate power of 8 (80% of maximum capacity) is represented as ({i = 1, t = GEN, c = 10}, 8). This approach allows us to easily simulate the on/off state and the stability of the power source.

In this component, the transition ”gen” fires when taking one NODE_POWER token from the place “Generator”, this color token represents a generator and its associated power generation. And a POWER token from the place “Generated”, which represents the total amount of electricity that has been produced and stored. The function fn_gen will sum the amount of electricity available from the generator and the amount of electricity available in the place “Generated” to create a new total.

Figure 5 depicts the state of the grid implemented on the CPN Tool after the transition “gen” fires once upon receiving G2 tokens ({i = 2, t = GEN, c = 5}, 5) (from the Generator place) and 0 power (the token 1‘0 in the Generated place) to generate 5 powers (the new token 1‘5 in the Generated place and no more token of G2 in the Generator place).

Listing 3

Three functions are used in the CPN

19 fun fn_gen ( p1 : POWER, p2 : POWER) = p1+ p2 ;

20 fun f n _c o n s ( n : NODE, p : POWER) =( n , p +(# c ( n ) ) ) ;

21 fun f n _t r a n s ( n : NODE, p :POWER) = p −(# c ( n ) ) ;

After being successfully generated, the electric power is ready to be transmitted and consumed using the transmission component. The “Consumer” place in Figure 6 contains all consumers of the grid with initial configuration. For example, the Consumer C2 (ID is 4, the demand for power is 6, and the amount of power received is 0) is represented as ({i = 4, t = CON, c = 6}, 0). Transition “trans” fires when it receives one token from place “Generated” and one from place “Consumer”. The function fn_trans and fn_cons are used for transferring and consuming power between two places “Generated” and “Consumer” Figure 7 describes a state of the grid when the place Consumer C2 received 6 powers (the token is changed to 1‘({i = 4, t = CON, c = 6}, 6).

Figure 8 shows the complete model of the sample smart grid. It is clear that the CPN model is small regardless of the complexity of the smart grid.

State Space

The state space in CPN is a set of possible configurations that system can have. For the demonstration case study 01, it is a collection of potential states of the grid in Figure 2. In this work, we use the built-in State Space module in CPN Tool to examine state space and Graphviz8 library in Fig. 9 for exporting state space to a Dotfile (*.dot), then visualize a graph from the Dotfile in Figure 10.

In our case, nodes named from 40, 42 to 48 are the final states of the grid, when there is no more firing. For example, node 40 in Listing 5 shows a result when Consumers 1, 2, and 3 receive 0, 18, and 0 powers respectively and 3 redundant powers (token 1‘3) is still at the ”Generated” place. This is not the success of the smart grid, absolutely.

Listing 4

A part of State space report file

1. S t a t i s t i c

2. −−−−−−−−−−−−−−−

3. S t a t e Space

4. Nodes

5. Arcs

6. Secs

7. S t a t u s : F u l l

8. Scc

9. Nodes

10. Arcs

11. Secs

12. . . .

Figure 9 represents a block of code in the CPN tool for exporting state space to the “StateSpace.dot” file. Figure 11 shows a part of the full state space in Figure 10.

Listing 4 shows that the state space of case 01 consists of 48 nodes and 96 arcs. The running time for the analysis of this state space was almost zero seconds and the state space was fully analyzed.

Listing 5

A part of State space .dot file

1. d i g r a p h _c p n _t o o l s _g r a p h {

2. N40 [ l a b e l = 4 0 :

3. s g r i d ’ G e n e r a t e d 1 : 1 ‘ 3

4. s g r i d ’ G e n e r a t o r 1 : empty

5. s g r i d ’ Consumer 1 :

6. 1 ‘ ({ i = 4 , t = CON, c = 6 } , 0) ++

7. 1 ‘ ({ i = 5 , t = CON, c = 9 } , 18 ) ++

8. 1 ‘ ({ i = 6 , t = CON, c = 6 } , 0 ) ]

9. N42 [ l a b e l = 4 2 : . . . ]

10. . . .

11. N1 −

12. { p2 = 0 , gen ={ i = 2 , t =GEN, c = 5 } , p1 =5} ]

13. N1 −> N3 [ l a b e l = A2 : 1−>3: gen

14. { p2 = 0 , gen ={ i = 3 , t =GEN, c = 6 } , p1 =6} ]

15. N1 −> N2 [ l a b e l = A1 : 1−>2: gen

16. { p2 = 0 , gen ={ i = 1 , t =GEN, c = 10 } , p1 =10} ]

17. . . .

Experimental setup

We aim to show how our suggested method can model a realistic version of a smart grid in this section. The grid’s setup in two different case studies is presented in Table 3.

In case study 02, we simulate the unstable power supply and the stable consumer demand. For example, Generator G1 can vary its capacity from 80% to 100% (9 to 12 power). By this simulation, the state space can be used to analyze situations such as when all consumers ask for their demands, then what are the power production levels of all generators.

For case study 03, some power generators may be shut down randomly to simulate network failures.

Smart Grid modeling discussion

Petri nets or Colour Petri nets have been used to model and verify smart grids in earlier research22. They all aim to mimic the network structure as closely as possible and use some verification methods to check some required properties. For instance, in22, all generators are places in a Petri net. This is convenient for engineers to simulate the nets as they know the topologies well. However, for big networks, the Petri nets are too complex to be shown and simulated and too difficult to be updated. Even the work in 24 that uses CPN to model grids still has large models when it concentrates on describing detailed/local electrical transformer areas to find and locate illegal loads. In our proposed approach, all generators (and their parameters) are color tokens, and the whole topology is reduced to a few simple components with flexible configurations. For example, the net in 22 with 11 generator nodes (P0 to P11) can be represented using our approach with only one node (Node P using the color token [{i=0, p=1}, {i=1, p=1, {i=2, p=4}] in which i is the name of a node, p means power) as illustrated in Figure 12.

Therefore, our models are easy to be updated and re- configured. Tools to convert from a smart grid to our net will be provided.

Experimental results and discussion

In case 02, the report consists of 367 nodes and 5 474 arcs. There are 6 nodes where the consumers receive their desired amount of power. These are our destination nodes. Of course, we need to travel in the state space to determine the paths from the initial node to the final node. Those paths are the configurations for the smart grid to be successfully operated.

For case 03, the state space consists of 536 nodes and 13 691 arcs, much more nodes and arcs compared to that of case

02. There are still 6 destination nodes to indicate the success of the configuration of the smart grid. However, the running time and computer resources from finding such “successful configurations” are still small, almost zero seconds.