形式化自动测试在计算机联锁系统中的应用研究

Research on the Application of Formal Automatic Test in Computer Interlocking System

通过研究形式化自动测试方法在计算机联锁系统中的应用,采用基于Prover iLock形式化工具、面向对象的PiSPEC高级语言编制测试脚本,将对联锁功能场景的测试延伸到对联锁逻辑变量的跟踪。形式化自动测试不仅可以测试系统功能,还可以检查联锁逻辑规则及联锁数据的正确性。本文阐述了基于对象模型的形式化自动测试方案,根据测试实例详细介绍了测试用例分解、用例执行结果以及可追溯的中间过程。结果表明:形式化自动测试能够提高测试效率,并且生成的测试用例对联锁测试对象的覆盖率达到了100%。

This paper studies the application of formal automatic test method in computer interlocking system. Based on Prover i Lock formalized tool and using object-oriented PiSPEC high-level language to compile the test script, the testing of Interlocking functional scenarios is extended to the tracing of Interlocking logic variables. Formal automatic test can not only test the system function, but also check the correctness of Interlocking logic rules and data. The formal automatic test scheme is described based on object model. According to the test examples, the decomposition of test cases, the execution results of test cases and the traceable intermediate process are introduced in detail. The results show that formal automatic testing can improve test efficiency, and the generated test cases cover 100% of Interlocking test objects.