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

doi:10.3969/j.issn.0372-2112.2013.11.026

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

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

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

1. 同济大学电子与信息工程学院, 上海 201804;
2. 嵌入式系统与服务计算教育部重点实验室, 上海 201804

收稿日期:2012-11-26 修回日期:2013-04-27 出版日期:2013-11-25
- 通讯作者:
- 万勇兵
- 作者简介:
- 徐中伟 男，1964年6月出生于江苏无锡.现为同济大学电子与信息工程学院信息与通信工程系教授、博士生导师.从事安全软件验证、测试与评估方面的研究工作. E-mail：xuzhongweish@163.com
- 基金资助:
- 国家自然科学基金 (No.61075002，No.61273180）; “十二五”国家科技支撑资助项目 (No.2011BAG01B03）; 铁道部科技重点资助项目 (No.2009X002-A）

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

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

1. School of Electronics & Information Engineering, Tongji University, Shanghai 201804, China;
2. The Key Laboratory of Embeddedsystem and Service Computing Ministry of Education, Shanghai 201804, China

Received:2012-11-26 Revised:2013-04-27 Online:2013-11-25 Published:2013-11-25
- Supported by:
- National Natural Science Foundation of China (No.61075002, No.61273180); Program Sponsered by National Science & Technology Pillar Program during the 12th Five-year Plan Period (No.2011BAG01B03); Key Science and Technology Funded Projects of Ministry of Railways (No.2009X002-A)

摘要/Abstract

摘要： 系统一致性测试用来验证和确认系统实现的正确性.针对实时系统在进行数据处理时受到时间约束，容易导致状态空间爆炸的问题，提出一种符号化测试生成方法.首先对符号变迁系统和时间自动机进行扩展，建立一种新的符号语义模型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.

Key words: real-time system, conformance test, time safety input-output symbolic transition system, symbolic test generation, test case generation

中图分类号:

TP301

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

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.

参考文献

[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.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020, 48(12): 2417-2424.
[2]	杨超, 郭云飞, 扈红超, 刘文彦, 霍树民, 王亚文. 基于符号执行的软件缓存侧信道脆弱性检测技术[J]. 电子学报, 2019, 47(6): 1194-1200.
[3]	郭曦, 王盼. 基于依赖条件重构的程序符号值分析方法[J]. 电子学报, 2019, 47(3): 630-635.
[4]	赵祖威, 冯世宁, 汤恩义, 陈鑫, 李宣东, 潘敏学, 赵晨. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.
[5]	徐超, 陈勇, 葛红美, 何炎祥. 基于符号执行的能耗错误检测方法[J]. 电子学报, 2016, 44(5): 1040-1050.
[6]	王志, 贾春福, 刘伟杰, 王晓初, 张海宁, 于晓旭, 陈喆. 一种抵抗符号执行的路径分支混淆技术[J]. 电子学报, 2015, 43(5): 870-878.
[7]	吴以凡, 张桦, 戴国骏. 面向多处理器资源预留的实时程序划分方法[J]. 电子学报, 2014, 42(4): 717-722.
[8]	王令赛, 姜淑娟, 张艳梅, 于巧. 基于正交搜索的粒子群优化测试用例生成方法[J]. 电子学报, 2014, 42(12): 2345-2351.
[9]	王颖, 谷利泽, 杨义先, 董宇欣. EWFT:基于程序执行过程的白盒测试工具[J]. 电子学报, 2014, 42(10): 2016-2023.
[10]	刘铮;赵海;张骞. 设备级OS中任务调度的IO抖动优化策略[J]. 电子学报, 2010, 38(11): 2555-2560.
[11]	赵明, 赵海, 张文波, 张浩华, 罗桂兰, 孙佩刚. 针对弱硬实时系统的DRM调度算法[J]. 电子学报, 2008, 36(1): 70-75.
[12]	李书浩, 王戟, 齐治昌, 董威, . 一种面向性质的实时系统测试方法[J]. 电子学报, 2005, 33(5): 827-834.
[13]	董文莉, 孟洛明, 邱雪松. 基于tML/消息队列的网络管理接口一致性测试方法[J]. 电子学报, 2005, 33(1): 22-25.
[14]	张玉军, 李忠诚. 移动IPv6测试中的层次化协议描述和测试生成方法[J]. 电子学报, 2004, 32(S1): 30-34.
[15]	王林章;李宣东;郑国梁. 一个基于UML协作图的集成测试用例生成方法[J]. 电子学报, 2004, 32(8): 1290-1296.