Testing the Fault Tolerance of a Backup Protection System Using SPIN

摘要

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 of our evolving critical infrastructure, new challenges arise in the form of defending these assets. Cyber-attacks have occurred in modern times on smart grids, dismantling the communication of supervisory control and data acquisition networks across expansive regions. A 2014 study conducted by the Federal Energy Regulatory Commission (FERC) revealed that small-scale, coordinated cyber-attacks on only a few substations across the United States could result in cascading failures affecting the entire nation. In support of defending critical infrastructure, this paper tests the fault tolerance of a Wide-Area Backup Protection System (WABPS). The WABPS examined is a regional peer-to-peer model resembling the Institute of Electrical and Electronics Engineers (IEEE) 14-bus system. Each of the 15 lines in the system incorporate 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 that could occur from real-life attacks 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. This line of research will be progressively critical to smart grid and other critical infrastructure engineers, who must consider how their infrastructure reacts to adversity as systems become increasingly interdependent. Using the techniques in this article, complex failure scenarios can be investigated early in development phases using the model checking approach, rather than later due to real-life attacks.