CTCS-3级测试案例完备性的自动验证

摘要

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切换功能的相关测试案例作为实例，应用自动验证工具对其进行了完备性验证，发现了现有测试案例中可能存在的不足并提出了处理建议，验证了本文方法和工具的有效性。

目录

声明

致谢

摘要

1 引言

1．1 CTCS－3 级列车运行控制系统

1．2 研究背景及意义

1．3 相关研究现状

1．4 论文主要工作

2 CTCS-3 级测试案例完备性验证的关键问题分析

2．1 CTCS-3 级列控系统测试简介

2．1．1 CTCS-3 级列控系统测试过程概述

2．1．2 CTCS-3 级列控系统测试案例

2．2 需求跟踪关系建立问题的转化

2．3 CTCS-3 级测试案例完备性验证关键问题的确定

2．4 本章小结

3 基于Event-B和因果图法的测试案例完备性验证

3．1 CTCS-3 级测试案例的完备性验证方法设计

3．1．1 Event-B方法及Rodin平台

3．1．2 因果图法

3．1．3 基于Event-B和因果图法的测试案例完备性验证方法设计

3．2 基于Event-B的SRS建模及验证

3．3 从Event-B模型到因果图的模型转换

3．3．1 Event模型和因果图模型的对应关系分析

3．3．2 Event-B模型的改写规则设计

3．3．3 从Event-B模型到因果图的映射规则设计

3．4 基于改进遍历式回溯算法的SRS判定表生成

3．5 测试案例的因果图建模及判定表生成

3．6 测试案例完备性衡量依据的确定

3．6．1 基于SRS判定表的测试充分性准则

3．6．2 基于SRS判定表的覆盖域生成

3．7 测试案例完备性对比验证的流程设计

3．8 本章小结

4 CTCS-3 级测试案例完备性自动验证工具的设计与实现

4．1 CTCS-3 级测试案例完备性自动验证工具的功能需求分析

4．2 CTCS-3 级测试案例完备性自动验证工具的总体设计

4．3 模型转换模块的设计与实现

4．4 因果图建立模块的设计与实现

4．5 判定表生成模块的设计与实现

4．6 完备性对比验证模块的设计与实现

4．7 本章小结

5 实例验证

5．1 待机模式下模式转换功能测试案例的完备性验证

5．1．1 待机模式下模式转换功能简介

5．1．2 待机模式下模式转换功能SRS的Event-B建模及验证

5．1．3 待机模式下模式转换功能Event-B模型的转换及判定表生成

5．1．4 待机模式下模式转换功能测试案例的因果图建模及判定表生成

5．1．5 待机模式下模式转换功能测试案例的完备性验证结果

5．2 RBC切换功能测试案例的完备性验证

5．2．1 RBC切换功能简介

5．2．2 RBC切换功能SRS的Event-B建模及验证

5．2．3 RBC切换功能Event-B模型的转换及判定表生成

5．2．4 RBC切换功能测试案例的因果图建模及判定表生成

5．2．5 RBC切换功能测试案例的完备性验证结果

5．3 本章小结

6 结论与展望

6．1 结论

6．2 展望

参考文献

图索引

表索引

作者简历及攻读硕士学位期间取得的研究成果

学位论文数据集