Automatic Test Generation of Large Boolean Expressions in Computer Based Interlocking System

Interlocking system is an important module to ensure traffic safety. However it is still very difficult to apply automatic testing in industrial application. In this paper, we propose an approach to generate test case automatically with the help of SMT Solver. First, we extract the yard specification written by boolean expressions from interlocking rules and configuration specification. And then a process to generate test cases based on the specification is given. Finally, We apply our approach to the interlocking system at LongXiLu station in China.