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

基金项目: 中国铁路总公司科研开发基金项目（W14D00301）。

详细信息

Automated test sequences generation for hot standby platform based on Event-B

1.
School of Electronics and Information Engineering, Beijing Jiaotong University, Beijing 100044, China;
2.
Department of Technology and Law, National Railway Administration, Beijing 100891, China;
3.
National Engineering Research Center for Rail Traffic Control System, Beijing Jiaotong University, Beijing 100044, China

摘要: 为了确保双机热备平台满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，可以有效地避免人工手动生成测试中存在的不足，提高测试效率。利用Event-B方法对双机热备平台进行形式化建模，通过证明验证模型的正确性，并进一步利用Ll算法生成基于模型、满足平台测试需求的测试序列集，对于确保测试过程的完备性、提高测试效率有一定意义。
- 双机热备平台 /
- 测试序列 /
- Event-B /
- Ll算法 /
- Rodin平台
Abstract: It is essential to ensure that the platform meets the functional requirements via function test. This paper discussed a model-based testing approach. The formal model of the platform was established by refinement in Event-B. Then, the correctness of the model was verified by mathematical proofs. The test sequences that were generated using Ll algorithm based on the Event-B model could be targeted to meet the test requirements which could help to ensure the completeness, and improve the efficiency of the test.
- hot standby platform /
- test sequence /
- Event-B /
- L1Algorithm /
- Rodin platform

[1]	林福栋. 基于COTS 和软件差异性的双机热备平台的设计与实现[D]. 北京：北京交通大学, 2011.
[2]	金丹, 王化深, 马连川, 等. 双机热备平台测试序列自动生成方法的研究[J]. 铁道学报, 2013（8）：70-74.
[3]	闫剑平, 汪希时. 两种方式双机热备结构的可靠性和安全性分析[J]. 铁道学报, 2000（3）：124-127.
[4]	Abrial,J.-R. Modeling in Event-B: System and Software Engineer[M]. Britain: Cambridge University Press, 2010.
[5]	Malik,Q.A, Lilius,J, et al. Model-Based Testing Using Scenarios and Event-B Refinements[J]. Methods, Models and Tools for Fault Tolerance, 2009 (5454):177-195.
[6]	Abrial,J.-R. The B-Book: Assigning Programs to Meanings[M]. Britain: Cambridge University Press,1996.
[7]	Angluin,D. Learning regular sets from queries and conterexamples[J]. Information and Computation, 1987,75(2): 87-106.
[8]	Ipate,F, Dinca,I, et al. Model learning and test generation using cover automata[J]. The Computer Jouranl, 2014,58(5): 1140-1159.
[9]	Dinca,I, Ipate,F, et al. Learn and test for Event-B[C]. Proceedings of the 3rd International Conference on Abstract State Machines, 2012: 361- 364.