CTCS-3级列控系统作为确保高速铁路系统高效、安全运营的关键,有着极其严格安全性、可靠性要求。为了确保CTCS-3级列控系统满足《CTCS-3级列控系统需求规范(SRS) (v1.0)》中规定的功能需求,需要对其进行充分的测试,而《CTCS-3级列控系统测试案例(v3.0)》构成了测试过程的基础和标准。测试案例的完备性,即测试案例的设计可以覆盖全部的系统功能需求,是测试过程能够充分验证列控系统是否符合SRS规定的关键。因此,为了确保测试案例的完备性,本文提出了一种CTCS-3级列控系统测试案例完备性的验证方法。论文的主要工作如下：(1)对CTCS-3级列控系统的测试过程以及测试案例的生成方法和描述形式进行研究,明确了CTCS-3级列控系统测试案例完备性验证的主要需求,以及需要解决的关键问题。(2)通过对关键问题的分析,提出基于Event-B和因果图法的测试案例完备性验证方法。利用Event-B方法对SRS进行严格的形式化建模,并将建模结果转换为因果图形式,通过生成SRS判定表并对测试案例进行因果图建模和判定表生成,统一SRS和测试案例的描述方式,同时依据SRS判定表得到测试案例的完备性衡量依据,最终通过对比验证得出测试案例的完备性验证结果。(3)在对上述方法进行详细设计的过程中,为了实现模型转换,设计了Event-B模型的改写、映射规则；为了明确SRS和测试案例的对应关系,提出了利用SRS因果图模型内事件对测试案例进行建模的方法,并相应设计了基于SRS判定表的测试充分性准则和覆盖域；根据测试案例判定表和覆盖域,设计了测试案例完备性的对比验证流程,使验证结果便于工作人员的使用。(4)在设计上述测试案例完备性验证方法的基础上,结合Rodin建模平台设计并开发了CTCS-3级列控系统测试案例完备性的自动验证工具。利用车载设备待机模式下的模式转换功能和RBC切换功能的相关测试案例作为实例,应用自动验证工具对其进行了完备性验证,发现了现有测试案例中可能存在的不足并提出了处理建议,验证了本文方法和工具的有效性。