期刊文献+

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

A Symbolic Execution Method for Conformance Test Generation of Real-Time System
下载PDF
导出
摘要 系统一致性测试用来验证和确认系统实现的正确性.针对实时系统在进行数据处理时受到时间约束,容易导致状态空间爆炸的问题,提出一种符号化测试生成方法.首先对符号变迁系统和时间自动机进行扩展,建立一种新的符号语义模型TSIOSTS,基于该模型定义了时间一致性关系(tioco);然后以tioco关系为指导,结合符号化执行策略,生成被测系统模型的时间符号化测试行为树,并转化为测试用例;最后将提出的理论和方法应用于CTCS-3列控系统临时限速服务器的一致性测试中,验证了该方法的可行性和有效性. Conformance test is performed to verify and validate the correctness of a system implementa-tion .In view of eas-ily 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 pro-posed 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 .
出处 《电子学报》 EI CAS CSCD 北大核心 2013年第11期2276-2284,共9页 Acta Electronica Sinica
基金 国家自然科学基金(No.61075002 No.61273180) "十二五"国家科技支撑资助项目(No.2011BAG01B03) 铁道部科技重点资助项目(No.2009X002-A)
关键词 实时系统 一致性测试 时间安全输入输出符号变迁系统 符号执行 测试用例生成 real-time system conformance test time safety input-output symbolic transition system symbolic test genera-tion test case generation
  • 相关文献

参考文献18

  • 1Abdeslam E,Rachida D,Ferhat K.Timed Wp-method:testing real-time systems[J].IEEE Transactions on Software Engineering,2002,28(11):1023-1038.
  • 2Moez K,Stavros T.Conformance testing for real-time systems[J].Formal Methods in Systems Design,2009,34(3):238-304.
  • 3Constant 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. 被引量:1
  • 5陈伟,薛云志,赵琛,李明树.一种基于时间自动机的实时系统测试方法[J].软件学报,2007,18(1):62-73. 被引量:14
  • 6Rachel 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.
  • 7Styp 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. 被引量:2
  • 9Adjir 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.
  • 10Krichen 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.

二级参考文献57

  • 1王之梁,吴建平,尹霞.基于通信多端口有限状态机的协议互操作性测试生成研究[J].计算机学报,2006,29(11):1909-1919. 被引量:13
  • 2W Simpson.The Point-to-Point Protocol(PPP) [S].RFC1661,1994.
  • 3B Lloyd.PPP Authentication Protocols [S].RFC1334,1992.
  • 4W Simpson.PPP Challenge Handshake Authentication Protocol (CHAP) [S].RFC1994,1 996.
  • 5G McGregor.The PPP Internet Protocol Control Protocol (IPCP) [S].RFC1332,1992.
  • 6K Sklower.The PPP Multilink Protocol (MP) [S].RFC1990,1996.
  • 7W Simpson.PPP Link Quality Monitoring [S].RFC1989,1996.
  • 8吴建平.形式化的协议一致性测试研究 [D].北京:清华大学,1996.
  • 9ISO.Information Technology;Open System Interconnection;Conformance Testing Metho dology and Framework.ISO-9646:Part 3-The Tree and Tabular Combined Notation [ S].ISO,1996.
  • 10朱三元,等.网络通信软件设计指南 [M].北京:清华大学出版社,1998.

共引文献14

同被引文献31

  • 1Mallet F,André C.On the semantics of UML/MARTE clock constraints[A].IEEE International Symposium on Object/ Component/Service-Oriented Real-Time Distributed Computing[C].Tokyo:IEEE Computer Society,2009.305-312.
  • 2André C,Mallet F.Specification and verification of time requirernents with CCSL and Esterel[J].ACM SIGPLAN Notices.2009,44(7):167-176.
  • 3Mallet F.Clock constraint specification language:specifying clock constraints with UML/MARTE[J].Innovations in Systems and Software Engineering.2008,4(3):309-314.
  • 4Mallet F,De Simone R.MARTE:A profile for RTE systems modeling,analysis and simulation[A].Proceedings of the 1st International Conference on Simulation Tools and Tochniques for Communications,Networks and Systems & Workshops[C].Marseille:ACM Press,2008.1-8.
  • 5Woodcock J,Larsen P G,Bicarregui J,et al.Formal methods:Practice and experience[J].ACM Computing Surveys,2009,41 (4):1-40.
  • 6Quadri I R,Gamatié A,Boulet P,et al.Expressing embedded systems configurations at high abstraction levels with UML MARTE profile:advantages,limitations and alternatives[J].Journal of Systems Architecture.2012,58(5):178-194.
  • 7Didier A,Farias A,Mota A.Checking Z data refinements using traces refinement[A].Proceedings of the Eleventh Brazilian Symposium on Formal Methods[C].Amsterdam:Elsevier,2009.129-148.
  • 8Derrick J,North S,Simons A J H.Z2SAL-Building a Model Chocker for Z[A].Abstract State Machines,B and Z[C].Berlin:Springer-Verlag,2008.280-293.
  • 9Rasch H,Wehrheim H.Checking consistency in UML diagrams:classes and state machines[A].Formal Methods for open,Object-based Distributed Systems[C].Berlin:SpringerVerlag,2003.229-243.
  • 10Rasch H,Wehrheim H.Checking the validity of scenarios in UML models[A].Formal methods for open,object-based distributed systems[C].Berlin:Springer-Verlag,2005.67-82.

引证文献3

二级引证文献30

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部