Satisfiability Verification of Engineering Data Safety Rules of Balise based on ROBDD

Engineering data safety pervades the balise telegram compilation, which affects the railway traffic safety. The existing method to ensure data safety is to verify that whether the data conform to the specific verification rules generated based on the balise application principles and engineering data compilation specifications. However, these rules are described by natural language, which are characterized by ambiguity and scarcity. The situation often arises where insufficient verifications of engineering data may lead to data safety problems in most cases. To address this problem above, implicit logic rules are explored ground on the constraints between every pair of data, and modelled as a Boolean function firstly. Then, the Reduced Ordered Binary Decision Diagram (ROBDD) construction and depth-first searching algorithm are performed to verify the satisfiability of the rules. Compared with the original ones, the extracted authenticated logic rules have promising results in the accuracy of data checking, and can further improve the safety of engineering data.