一种符号化执行的实时系统一致性测试生成方法

doi:10.3969/j.issn.0372-2112.2013.11.026

PDF(1940 KB)

电子学报 ›› 2013, Vol. 41 ›› Issue (11) : 2276-2284. DOI: 10.3969/j.issn.0372-2112.2013.11.026

学术论文

一种符号化执行的实时系统一致性测试生成方法

万勇兵^1,2, 徐中伟^1,2, 梅萌¹

作者信息 +

A Symbolic Execution Method for Conformance Test Generation of Real-Time System

WAN Yong-bing^1,2, XU Zhong-wei^1,2, MEI Meng¹

Author information +

文章历史 +

摘要

系统一致性测试用来验证和确认系统实现的正确性.针对实时系统在进行数据处理时受到时间约束，容易导致状态空间爆炸的问题，提出一种符号化测试生成方法.首先对符号变迁系统和时间自动机进行扩展，建立一种新的符号语义模型TSIOSTS，基于该模型定义了时间一致性关系（tioco）；然后以tioco关系为指导，结合符号化执行策略，生成被测系统模型的时间符号化测试行为树，并转化为测试用例；最后将提出的理论和方法应用于CTCS-3列控系统临时限速服务器的一致性测试中，验证了该方法的可行性和有效性.

Abstract

Conformance test is performed to verify and validate the correctness of a system implementa- tion.In view of easily causing the problem of state space explosion,and due to time constraint in data processing for real-time system,a symbolic test generation method is proposed.Firstly,symbolic transition systems and timed automata are extended to establish a semantic model TSIOSTS,based on which an extension of timed conformance relation tioco is defined.Then,with tioco and the symbolic execution strategy,a symbolic timed behavior tree of the system model under test is yielded and transformed into test cases.Finally,the proposed method is applied to conformance test of temporary speed restriction server of the CTCS-3 train control system,and the results present feasibility and validity of the method.

导出引用

万勇兵, 徐中伟, 梅萌. 一种符号化执行的实时系统一致性测试生成方法[J]. 电子学报, 2013, 41(11): 2276-2284. https://doi.org/10.3969/j.issn.0372-2112.2013.11.026

WAN Yong-bing, XU Zhong-wei, MEI Meng. A Symbolic Execution Method for Conformance Test Generation of Real-Time System[J]. Acta Electronica Sinica, 2013, 41(11): 2276-2284. https://doi.org/10.3969/j.issn.0372-2112.2013.11.026

中图分类号： TP301

参考文献

[1] Abdeslam E,Rachida D,Ferhat K.Timed Wp-method:testing real-time systems[J].IEEE Transactions on Software Engineering,2002,28(11):1023-1038.
[2] Moez K,Stavros T.Conformance testing for real-time systems[J].Formal Methods in Systems Design,2009,34(3):238-304.
[3] Constant C,Thierry J,Marchand H.Integration formal verification and conformance testing for reactive system[J].IEEE Transactions on Software Engineering,2007,33(8):558-574.
[4] 胡宇,吴建平,等.PPP一致性测试研究[J].电子学报,2002,30(8):1242-1245. HU Yu,WU Jian-ping,et al.PPP conformance testing research[J].Acta Electronica Sinica,2002,30(8):1242-1245.(in Chinese)
[5] 陈伟,薛志云,赵琛,李明树.一种基于时间自动机的实时系统测试方法[J].软件学报,2007,18(1):62-73. CHEN Wei,XUE Yun-Zhi,ZHAO Chen,LI Ming-Shu.A method for testing real-time system based on timed automata[J].Journal of Sofware,2007,18(1):62-73.
[6] Rachel C O,Tim G.A practical and complete algorithm for testing real-time systems[A].Proc of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems[C].Berlin:Springer-Verlag Press,1998.251-261.
[7] Styp S V,Bohnenkamp H,Schmaltz J.A conformance testing relation for symbolic timed automata[A].Lecture Notes in Computer Science[C].Berlin:Springer-Verlag Press,2010.243-255.
[8] 李书浩,王戟,齐治昌.一种面向性质的实时系统测试方法[J].电子学报,2005,33(5):827-834. LI Shu-hao,WANG Ji,QI Zhi-chang.An approach to property-oriented testing of real-time systems[J].Acta Electronica Sinica,2005,33(5):827-834.(in Chinese)
[9] Adjir N,Pierre S S,Kamel M R.Time optimal real-time test case generation using prioritized time petri net[J].Proceedings of First International Conference on Advances in System Testing and Validation Lifecycle[C].New York:IEEE Press,2009.110-116.
[10] Krichen M,Tripakis S.State identification problems for timed automata[A].Proceedings of the 17th International Conference on Testing of Communicating Systems[C].Berlin:Springer-Verlag Press,2005.175-191.
[11] Khoumsi M.Complete test graph synthesis for symbolic real-time systems[J].Electronic Notes in Theoretical Computer Science,2005,30(5):79-100.
[12] Thierry J.Symbolic model-based test selection[J].Electronic Notes in Theoretical Computer Science,2009,240(7):167-184.
[13] ISO/IEC.Information Technology,Open Systems Interconnection,Conformance Testing Methodology and Framework[S].ISO/IEC 9646,1991.
[14] 王之梁,尹霞,景传明.一种形式化的实时协议互操作性测试方法[J].中国科学E辑,2008,38(10):1614-1635.
[15] King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394.
[16] Gaston C,Gall P L,Rapin N,Touil A.Symbolic execution techniques for test purpose definition[A].Lecture Notes in Computer Science[C].Berlin:Springer-Verlag Press,2006.1-18.
[17] Andrade W L,Machado P D L,Thierry J.Abstracting time and data for conformance testing of real time systems[A].The 4th Internal Conference on Software Testing,Verification and Validation Workshop[C].New York:IEEE Press,2011.9-17.
[18] Elisabeth J,Martin W,et al.When BDDs fail:conformance testing with symbolic execution and SMT solving[A].The 3rd International Conference on Software Testing,Verification and Validation Workshop[C].New York:IEEE Press,2010.479-488.