随着无线电技术的飞速发展,基于精确的定位技术和高速、实时通信技术的CBTC(Communication-Based Train Control,基于通信的列车控制)系统成为轨道交通运行控制系统发展的方向。区域控制器作为CBTC系统地面的核心设备,需要具备极高的安全性与可靠性,因此在投入使用之前必须经过严格的功能和性能测试。目前在对区域控制器进行测试时采用的测试序列仍然依靠人工的方式进行生成,由于人为因素的不确定性以及人工方式编制的测试序列很难做到完备性测试,系统可靠性及安全性无法得到彻底保证。因此,对区域控制器测试序列的自动生成方法进行研究有重要意义。论文基于区域控制器的形式化模型研究了区域控制器的测试序列自动生成方法。首先,对区域控制器进行功能分析,建立区域控制器的时间自动机模型。形式化建模消除了自然语言的二义性,便于计算机识别,为测试序列的自动生成创造了条件。然后,利用UPPAAL对建立的时间自动机模型进行模拟仿真,同时根据区域控制器的功能性及实时性要求,编写BNF验证语句对模型进行验证,为生成正确的测试序列提供可能性。接着分析建立的时间自动机模型文件的格式特点,针对其特定的信息存储格式,提取其中的关键字以获取区域控制器的状态信息及变迁关系,组合生成测试案例。然后基于区域控制器的功能特征,利用优先级设置及重复性标记将生成的测试案例首尾相连串接成符合区域控制器工作流程及测试规则的测试序列。最后,基于Microsoft Visual Studio丰富的功能库资源编写应用程序,实现输入区域控制器的时间自动机模型后,对模型信息自动提取,以及输入功能特征对应的初始状态与结束状态后,测试序列的自动生成。通过将自动提取的区域控制器模型信息与人工提取的信息对比可知文中设计的信息提取方法能够完成对模型变迁信息的全覆盖提取,由此可以证明测试案例的完备性;自动生成的测试序列与人工串接生成的结果一致,证明生成的测试序列在保证全覆盖的同时可以将测试案例的重复使用率降至最低。同时,测试序列的自动生成可以有效避免人工生成过程中的不确定性风险。