Abstract
Smart electrical grids refer to networked systems for distributing and transporting electricity from producers to consumers, by dynamically configuring the network through remotely controlled (dis)connectors. The consumers of the grid have typically distinct priorities, e.g., a hospital and an airport have the highest priority and the street lighting has a lower priority. This means that when electricity supply is compromised, e.g., during a storm, then the highest priority consumers should either not be affected or should be the first for whom electricity provision is recovered. In this paper, we propose a general formal model to study the provability of such a property. We have chosen Event-B as our formal framework due to its abstraction and refinement capabilities that support correct-by-construction stepwise development of models; also, Event-B is tool supported. Being able to prove various properties for such critical systems is fundamental nowadays, as our society is increasingly powered by dynamic digital solutions to traditional problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Back, R., Sere, K.: From Modular Systems to Action Systems. Software - Concepts and Tools 13, 26–39 (1996)
Back, R., Sere, K.: Superposition Refinement of Reactive Systems. Formal Asp. Comput. 8(3), 324–346 (1996)
Bryans, J.W., Wei, W.: Formal Analysis of BPMN Models Using Event-B. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 33–49. Springer, Heidelberg (2010)
Calderaro, V., Hadjicostis, C.N., Piccolo, A., Siano, P.: Failure identification in smart grids based on Petri Net modeling. IEEE Transactions on Industrial Electronics 58(10), 4613–4623 (2011)
Clark, A., Pavlovski, C.: Wireless Networks for the Smart Energy Grid: Application Aware Networks. In: Proceedings of the International Multi Conference of Engineers and Computer Scientists, vol. 2 (2010)
Craigen, D., Gerhart, S., Ralson, T.: Case Study: Paris Metro Signaling System. In: Proceedings of IEEE Software, pp. 32–35. IEEE (1994)
Event-B and the Rodin Platform, http://www.event-b.org/ (accessed January 2014)
Fang, X., Misra, S., Xue, G., Yang, D.: Smart grid - the new and improved power grid: A survey. IEEE Communications Surveys and Tutorials 14(4), 944–980 (2012)
Farhangi, H.: The path of the smart grid. IEEE Power & Energy Mag. 8(1), 18–28 (2010)
Salehi Fathabadi, A., Rezazadeh, A., Butler, M.: Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 328–342. Springer, Heidelberg (2011)
Gharavi, H., Ghafurian, R.: Smart grid: The electric energy system of the future. Proc. IEEE 99(6), 917–921 (2011)
He, M., Zhang, J.: Fault detection and localization in smart grid: A probabilistic dependence graph approach. In: IEEE SmartGridComm 2010, pp. 43–48 (2010)
Horsmanheimo, S., Maskey, N., Kokkoniemi-Tarkkanen, H., Savolainen, P., Tuomimäki, L.: Evaluation of Interdependencies between Mobile Communication and Electricity Distribution Networks in Fault Scenarios. In: IEEE ISGT Asia 2013 (2013)
Horsmanheimo, S., Kamali, M., Kolehmainen, M., Neovius, M., Petre, L., Rönkkö, M., Sandvik, P.: On Proving Recoverability of Smart Electrical Grids. Tech. Rep. 1096, TUCS – Turku Centre for Computer Science (2013)
Kamali, M., Laibinis, L., Petre, L., Sere, K.: A Distributed Design of a Network Recovery Algorithm. International Journal of Critical Computer-Based Systems 4(1), 45–68 (2013)
Kamali, M., Laibinis, L., Petre, L., Sere, K.: Formal development of wireless sensor-actor networks. Science of Computer Programming 80, 25–49 (2014)
LaCommare, K., Eto, J.: Cost of power interruptions to electricity consumers in the United States. Tech. rep., Ernest Orlando Lawrence Berkeley National Laboratory, lBNL-58164 (2006)
Luan, W., Sharp, D., Lancashire, S.: Smart grid communication network capacity planning for power utilities. In: Proceedings of Transmission and Distribution Conference and Exposition, pp. 1–4. IEEE (2010)
Moslehi, K., Kumar, R.: A Reliability Perspective of the Smart Grid. IEEE Transaction on Smart Grid 1(1), 57–64 (2010)
Petre, L., Sandvik, P., Sere, K.: Node Coordination in Peer-to-Peer Networks. In: Sirjani, M. (ed.) COORDINATION 2012. LNCS, vol. 7274, pp. 196–211. Springer, Heidelberg (2012)
Tate, J., Overbye, T.: Double line outage detection using phasor angle measurements. In: Power & Energy Society General Meeting, PES 2009, pp. 1–5. IEEE (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Horsmanheimo, S. et al. (2014). On Proving Recoverability of Smart Electrical Grids. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)