高铁信号系统安全关键功能测试建模方法

doi:10.3969/j.issn.0258-2724.20200378

李耀^1,,
张晓霞^1,,,
郭进²,
张亚东²

1.
电子科技大学光电科学与工程学院, 四川成都 611731
2.
江南娱乐网页版入口官网下载安装信息科学与技术学院, 四川成都 611756

基金项目:国家自然科学基金（61703349）

详细信息

作者简介:
李耀（1985—），男，博士研究生，研究方向为铁路信号系统安全关键软件测试，E-mail：ly_9967@163.com

通讯作者:
张晓霞（1961—），女，教授，研究方向为通信技术可靠性，E-mail：xxzhang@uestc.edu.cn

中图分类号:U283
计量
- 文章访问数:536
- HTML全文浏览量:352
- PDF下载量:16
- 被引次数:0
出版历程
- 收稿日期:2020-06-12
- 修回日期:2020-11-20
- 网络出版日期:2021-11-15
- 刊出日期:2020-12-25

Testing Modeling Method for Safety Critical Function of High-Speed Railway Signal System

1.
School of Optoelectronic Science and Engineering, University of Electronic Science and Technology of China, Chengdu 611731, China
2.
School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China

摘要

摘要:
测试模型是高铁信号系统安全关键功能测试用例编制的重要基础，针对高铁信号系统安全关键功能测试建模过程中描述信号系统领域特征不够全面的问题，提出时间状态机测试建模理论和测试用例生成方法. 分析高铁信号系统测试建模的特点，提出信号系统安全关键功能测试模型的建模需求；以有限状态机理论为研究基础，结合功能逻辑和时钟约束提出时间状态机建模方法，采用Z规格说明语言给出时间状态机的形式化定义；将时间状态机转换为时间自动机，证明转换之间的一致性，并基于时间自动机的测试理论自动生成测试用例，再以计算机联锁系统中的道岔转换功能为例，建立时间状态机测试模型并生成测试用例. 最后，将两种方法生成的测试案例进行对比，结果表明：在功能逻辑方面，基于时间状态机建模方法生成的测试案例100% 地覆盖了基于时间自动机建模方法生成的测试案例，并新增了16条具有时钟约束的测试案例，能够满足高铁信号系统安全关键功能测试建模的需求.
- 铁路信号系统/
- 建模方法/
- 时间状态机/
- Z语言/
- 时间自动机
Abstract:
Testing model is an important basis to create the test cases of safety critical function of high-speed railway signal system. To solve the problem that the characteristics of signal system are not fully represented in the modeling process of safety critical function test of high-speed railway signal system, the modeling theory of timed finite state machine (TFSM) and test case generation method are proposed. The characteristics in the test modeling of high-speed railway signal system is analyzed, and the modeling requirements are put forward. Then, based on the theory of finite state machine, a modeling method of TFSM is proposed by utilizing functional logic and clock constraints, and its formal definition is established with Z notation. Further, the TFSM is transformed into timed automata, which can prove the consistency between them, and test cases are automatically generated with timed automata based testing theory. The switch conversion function of the computer interlocking system is used as an example to build the testing model of TFSM and generate the test cases. The result shows that compared with the test cases generated by timed automata, in terms of functional logic, the test cases generated by TFSM can fully cover those generated by timed automata, and add 16 more test cases with clock constraints, showing that TFSM can meet the testing modeling requirements for the safety critical function of high-speed railway signal system.
- railway signal system/
- modeling method/
- timed finite state machine/
- Z notation/
- timed automata

HTML全文

图 1有限状态机示例

Figure 1.Example of finite state machine

下载: 全尺寸图片幻灯片

图 2TFSM与TA的测试用例的关系

Figure 2.Relationship of test cases between TFSM and TA

下载: 全尺寸图片幻灯片

图 3道岔定位选排测试模型

Figure 3.Testing model of switch subsystem

下载: 全尺寸图片幻灯片

图 4D_{TFSM_SW}等价的TA模型D_{TA_SW}

Figure 4.TA modelD_{TA_SW}equivalent toD_{TFSM_SW}

下载: 全尺寸图片幻灯片

表 1道岔子系统信号的含义

Table 1.Meaning of signals in the switch subsystem

信号	含义	信号	含义
g₁	反位请求	g₂	定位需求
g₃	正在转换	g₄	请求转换
g₅	道岔锁闭	g₆	选排一致
g₇	道岔定位	g₈	道岔未锁闭
g₉	道岔未在定位	g₁₀	道岔未转换
g₁₁	道岔定位操作

下载: 导出CSV

表 2D_{TFSM_SW}测试用例统计

Table 2.Test case statistics ofD_{TFSM_SW}

覆盖准则	用例总数/个	时钟约束用例/个
NC	1	1
EC	28	8
EPC	32	8
CPC	52	16

下载: 导出CSV

表 3D_{TFSM_SW}与D_{TA_SW}对比

Table 3.Comparison ofD_{TFSM_SW}andD_{TA_SW}

模型	状态/个	变迁/条	信号/个
D_{TFSM_SW}	9	15	11
D_{TA_SW}	9	37	11

下载: 导出CSV

表 4不同建模方法生成的测试用例对比

Table 4.Comparison of test cases generated by different modeling methods

建模方法	功能逻辑用例/个	时钟约束用例/条
TFSM	36	16
Petri	36	0
UML Statechart	36	0

下载: 导出CSV

表 5D_{TFSM_SW}具有时钟约束的测试案例

Table 5.Test cases with clock constraints ofD_{TFSM_SW}

序号	时钟约束测试案例	序号	时钟约束测试案例
1	g₂,g₈,g₉,g₁₀,x＞1,g₁	9	g₂,g₈,g₉,g₁₀,x＞1,g₉,x≥13
2	g₂,g₈,g₉,g₁₀,x＞1,g₃	10	g₂,g₈,g₉,g₁₀,x＞1,g1
3	g₂,g₈,g₉,g₁₀,x＞1,g₅	11	g₂,g₈,g₉,g₁₀,x＞1,g₇,x＜13,g₁
4	g₂,g₈,g₉,g₁₀,x＞1,g₇	12	g₂,g₈,g₉,g₁₀,x＞1,g₇,x＜13,g₁
5	g₁₁,g₈,g₉,g₁₀,x＞1,g₁	13	g₁₁,g₈,g₉,g₁₀,x＞1,g₉,x≥13
6	g₁₁,g₈,g₉,g₁₀,x＞1,g₃	14	g₁₁,g₈,g₉,g₁₀,x＞1,g₁
7	g₁₁,g₈,g₉,g₁₀,x＞1,g₅	15	g₁₁,g₈,g₉,g₁₀,x＞1,g₇,x＜13,g₁
8	g₁₁,g₈,g₉,g₁₀,x＞1,g₇	16	g₁₁,g₈,g₉,g₁₀,x＞1,g₇,x＜13,s₃,g₁

下载: 导出CSV

参考文献 (24)

[1]	上官伟,胡福威,袁敏,等. 基于弹复力效应的列控车载设备可靠性分析方法[J]. 铁道学报,2018,40(6): 75-82.doi:10.3969/j.issn.1001-8360.2018.06.010 SHANGGUAN Wei, HU Fuwei, YUAN Min, et al. Reliability analysis method for on-board equipment of train control system based on resilience effect[J]. Journal of the China Railway Society, 2018, 40(6): 75-82.doi:10.3969/j.issn.1001-8360.2018.06.010
[2]	袁磊,吕继东,刘雨,等. 一种全覆盖的列控车载系统测试用例自动生成算法研究[J]. 铁道学报,2014,36(8): 55-62.doi:10.3969/j.issn.1001-8360.2014.08.010 YUAN Lei, LÜ Jidong, LIU Yu, et al. Research on model-based test case generation method of onboard subsystem in CTCS-3[J]. Journal of the China Railway Society, 2014, 36(8): 55-62.doi:10.3969/j.issn.1001-8360.2014.08.010
[3]	吕继东,朱晓琳,李开成,等. 基于模型的CTCS-3级列控系统测试案例自动生成方法[J]. 江南娱乐网页版入口官网下载安装学报,2015,50(5): 917-927.doi:10.3969/j.issn.0258-2724.2015.05.023 LYU Jidong, ZHU Xiaolin, LI Kaicheng, et al. Model-based test case automatic generation of CTCS-3 train control system[J]. Journal of Southwest Jiaotong University, 2015, 50(5): 917-927.doi:10.3969/j.issn.0258-2724.2015.05.023
[4]	LI C L, LI K C, TANG T, et al. Model-based generation of safety test-cases for onboard systems[C]//2013 IEEE International Conference on Intelligent Rail Transportation Proceedings. Beijing: IEEE, 2013: 191-196.
[5]	魏柏全. 基于TAIO变异分析的新型列控系统安全功能测试评价研究[D]. 北京: 北京交通大学, 2018.
[6]	CHEN Lijie, ZHAO Tianshi, SUN Chao, et al. Test case generation method based on colored Petri net for train control system[C]//2018 3rd International Conference on System Reliability and Safety (ICSRS). Barcelona: IEEE, 2018: 1-5.
[7]	赵晓宇, 杨志杰, 吕旌阳. 基于有色Petri网的车载设备模式转换测试序列生成方法[J]. 中国铁道科学, 2017, 38(4): 115-123. ZHAO Xiaoyu, YANG Zhijie, LYU Jingyang, Test sequence generation method of mode transition for on-board equipment based on colored Petri net[J]. China Railway Science, 2017, 38(4): 115-123.
[8]	曹雅鑫. 基于UML状态图的列控中心轨道电路编码功能测试用例生成方法研究[D]. 成都: 江南娱乐网页版入口官网下载安装, 2017.
[9]	王秀玄. 基于UML的列控中心改变运行方向功能测试用例生成方法研究[D]. 成都: 江南娱乐网页版入口官网下载安装, 2016.
[10]	AMMANN P, OFFUTT J. Introduction[M]//Introduc- tion to Software Testing. Cambridge: Cambridge University Press, 2017: 3-24.
[11]	梅林. 形式化联锁软件测试技术研究[D]. 兰州: 兰州交通大学, 2014.
[12]	郭昊男. 新型列控系统车载ATP安全功能在线测试研究[D]. 北京: 北京交通大学, 2019.
[13]	富德佶. 基于模型的CTCS-3列控系统互联互通测试自动分析方法研究[D]. 北京: 北京交通大学, 2015.
[14]	谢林,杨扬. 基于模型的进路建立过程测试用例自动生成[J]. 铁道标准设计,2017,61(2): 109-116. XIE Lin, YANG Yang. Model-based automatic generation of test case of route establishment process[J]. Railway Standard Design, 2017, 61(2): 109-116.
[15]	HUANG Y S, CHUNG T H, CHEN C T. Modeling traffic signal control systems using timed colour Petri nets[C]//2005 IEEE International Conference on Systems, Man and Cybernetics. Waikoloa: IEEE, 2005: 1759-1764.
[16]	ZAID D H. Safecharts: a statecharts variant for safety-critical systems design[D]. Reading: University of Reading, 2005.
[17]	ANDRÉ C. Computing SyncCharts reactions[J]. Electronic Notes in Theoretical Computer Science, 2004, 88: 3-19.doi:10.1016/j.entcs.2003.05.007
[18]	李耀. 铁路信号系统安全关键软件建模与分析方法[D]. 成都: 江南娱乐网页版入口官网下载安装, 2018.
[19]	ZHANG Tao, HUANG Shaobin, HUANG Hongtao. An operational semantics for UML RT-statechart in model checking context[C]//2009 Fourth International Conference on Internet Computing for Science and Engineering. Harbin: IEEE, 2009: 12-18.
[20]	铁道部科学技术司, 铁道部运输局. CTCS-3级列控系统测试案例(V3.0): 科技运[2009] 59号[S]. 北京: [出版者不详], 2009.
[21]	铁道部科学技术司,铁道部运输局. CTCS-3级列控系统测试案例(V3.0):科技运[2009] 59号[S]. 北京: [出版者不详], 2009.doi:10.3969/j.issn.0258-2724.2015.01.005 LI Yao, CHEN Rongwu, GUO Jin, et al. Modeling and verification of TSSM-based CBTC zone controller for urban rail transit[J]. Journal of Southwest Jiaotong University, 2015, 50（1）: 27-35.doi:10.3969/j.issn.0258-2724.2015.01.005
[22]	张曙光. CTCS-3级列控系统总体技术方案[M]. 北京: 中国铁道出版社, 2008.
[23]	饶畅,李楠,张亚东,等. 铁路信号安全关键软件的组合测试序列集约简[J]. 江南娱乐网页版入口官网下载安装学报,2020,55(3): 596-603.doi:10.3969/j.issn.0258-2724.20190157 RAO Chang, LI Nan, ZHANG Yadong, et al. Combinatorial test sequence set reduction approach for railway signaling safety-critical software[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 596-603.doi:10.3969/j.issn.0258-2724.20190157
[24]	吴彪. 基于EFSM的测试用例自动生成方法的研究[D]. 杭州: 浙江理工大学, 2016.