Formal verification method and system for interlocking data security

A formal verification system for an interlocking data security, comprising:

• a general verification model building module, wherein the general verification model building module is configured to build an interlocking data formal verification general model and establish a mapping relation between a set security logical attribute in the interlocking data formal verification general model and an interlocking device, an interlocking logical parameter, and a station interlocking function in interlocking data;
• an interlocking data security conversion module connected to the general verification model building module, wherein the interlocking data security conversion module is configured to perform a security conversion on interlocking data to be verified according to the mapping relation to obtain general verification data required by the interlocking data formal verification general model;
• a formal security verification module connected to the interlocking data security conversion module, wherein the formal security verification module is configured to perform automatic verification on a verification object selected from the general verification data according to a selected verification algorithm;
• a formal counterexample verification and debugging module connected to the formal security verification module, wherein the formal counterexample verification and debugging module is configured to acquire and analyze a verification error issue list and perform counterexample verification and debugging on a counterexample description when the counterexample description exists in the verification error issue list;
• and
• an interlocking data security verification result generation module connected to the formal security verification module, wherein the interlocking data security verification result generation module is configured to generate an interlocking data security verification report according to an output result of the formal security verification module.