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 to the evolving critical infrastructure, new challenges arise in designing fault-tolerant 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 resilient 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 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 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.