辛 未，穆建成，马连川，3，曹 源，3

（1.北京交通大学 电子信息工程学院，北京 100044；2.国家铁路局 科技与法制司，北京 100891；3.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044）

基于Event-B的双机热备平台测试序列自动生成方法

辛 未1，穆建成2，马连川1，3，曹 源1，3

（1.北京交通大学 电子信息工程学院，北京 100044；2.国家铁路局 科技与法制司，北京 100891；3.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044）

为了确保双机热备平台满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，可以有效地避免人工手动生成测试中存在的不足，提高测试效率。利用Event-B方法对双机热备平台进行形式化建模，通过证明验证模型的正确性，并进一步利用Ll算法生成基于模型、满足平台测试需求的测试序列集，对于确保测试过程的完备性、提高测试效率有一定意义。

双机热备平台；测试序列；Event-B；Ll算法；Rodin平台

为了在高效运营的同时严格保证系统安全，轨道交通系统使用的设备需要达到相应的安全完整性等级（SIL）。双机热备平台是一种符合SIL2级要求的安全计算机平台，作为现代铁路信号系统的核心基础设备得到了广泛的应用[1～2]，安全计算机平台具有严格的安全性、可靠性要求[1～3]。为了确保其满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，对系统进行形式化建模、自动生成测试序列，可以有效地避免人工失误、提高测试效率，保证测试过程的完备性。……