Testing the Fault Tolerance of a Backup Protection System Using SPIN
Abstract:
This article advocates the use of automated model checking to find vulnerabilities in cyber-physical systems. Cyber-physical systems are increasingly prevalent in daily life. Smart grids, in particular, are becoming more interconnected and autonomously run. While there are advantages to the evolving critical infrastructure, new challenges arise in designing fault-toler-ant cyber-physical systems. Tools for automated model checking are a key asset in designing and evaluating cyber-physical systems and their components to maximize robustness and to pinpoint vulnerabilities so that they can be mitigated as early in the design process as possible. As a proof of concept for this model checking concept, this paper tests the fault tolerance of a Wide-Area Backup Protection System (WABPS). Each line in the WABPS incorporates a pair of autonomous agents, hosted on intelligent electronic devices (IEDs), which monitor the status of the line and make decisions regarding the safety of the grid. The IEDs coordinate their actions and share knowledge in a modern smart grid fashion. The SPIN model checker is used to evaluate how re-silient the WABPS is in responding to electric power faults, within the context of the IEEE 14-bus test case, when experiencing malfunctions and failures. Each of the 15 lines in the system incor-porate a pair of autonomous agents known as intelligent electronic devices (IEDs), which monitor the status of the line and make decisions regarding the safety of the grid. Various types of failures are simulated in the grid with the intent of determining how resilient the WABPS is in successfully responding to faults, despite malfunctions. Given that there are millions of scenarios of possible IED states and locations of faults across the 15 lines, the level of complexity of this problem rises at a commensurate rate. The SPIN model checker is used to execute every possible combination to determine what types of failures can occur, and how many, before the system is unable to properly clear a fault. With results tabulated, recommendations are made on how to improve the model. Using the techniques in this article, complex failure scenarios can be investigated, and fixes and tweaks can be applied early in development rather than in the later and more expensive phases of the design cycle.
AUTHORS
Department of Electrical and Computer Engineering Air Force Institute of Technology Dayton, Ohio,
United States
Lt. Kenneth James received his B.S. in Mathematics from the University of Texas at Austin in 2017, then his M.S. in Cyber Operations from the Air Force Institute of Technology in 2019. He currently serves as a Network Operations Officer at Osan Air Base, Republic of Korea. His research interests include computer security and automated tools to enhance and ensure correctness in mission-critical software systems.
Department of Electrical and Computer Engineering Air Force Institute of Technology Dayton, Ohio,
United States
Kenneth M. Hopkinson received his B.S. in 1997 from Rensselaer Polytechnic Institute in Troy, New York, and his M.S. and PhD degrees from Cornell University in 2002 and 2004, respectively, all in Computer Science. He is a Professor of Computer Science at the Air Force Institute of Technology in Dayton, Ohio. His interests include distributed systems, networks, simulation, and formal methods.
Published In
Journal of Information Warfare
The definitive publication for the best and latest research and analysis on information warfare, information operations, and cyber crime. Available in traditional hard copy or online.
Quick Links
Archive
