Model Checking of Cooperative Tripping Based on Timed Automata

Networked collaborative tripping can effectively reduce the construction complexity of the backup protection system, but there is still a lack of research on the reachability and real-time verification of the tripping algorithm. In this paper, the networked cooperative trip system is regarded as a reactive real-time system, and a method for verifying the cooperative characteristics of the protection system based on a timed automata is proposed. First, the timed automata are used to give the calculation model of the protection IED, the circuit breaker XCBR and the overall protection system, and then UPPAAL is used to model the model, and the description method of time characteristics is given, and the UPPAAL tool is used to verify the model. The algorithm model in the bus 12node system has been effectively verified. This method can complete the accessibility and real-time evaluation of the tripping algorithm, which is of great significance for reducing the hidden dangers in the system design.