Automatic Generation of Test Cases for Statechart Specification Based on the Conformance Testing Theory

doi:10.3969/j.issn.1007130X.2011.

Abstract

Abstract:

This paper studies testing semantics and automatic test case generation for

Statechart specification. Applying Tretmans’ approach to generate test cases for I/O automata

from labeled transition systems, we provide a solid mathematical basis for conformance testing

and automatic test case generation for Statechart specification. We introduce formal testing

semantics of Statechart specification that go beyond the semantics presented for formal

verification. These observable testing semantics can be used for general application, critical

application and realtime application. We also propose a formal conformance testing relation

based on presenting formal semantics and test hypothesis, and provide an algorithm which, for

a Statechart specification, generates a test suites. For finiteruns semantics the algorithm

can generate complete test suites, and for infiniteruns semantics only sound test suite can

be generated.

Key words: specification;implementation;conformance testing;test suite;test case generation;formal semantics;reactive system

MIAO Chunyu1,CHEN Lina2,ZHAO Jianmin2. Automatic Generation of Test Cases for Statechart Specification Based on the Conformance Testing Theory[J]. J4, 2011, 33(3): 82-89.

References

［1］Harel D. Statecharts: A Visual Formalism for Complex Systems［J］. Science of Computer

Programming, 1987, 8(3):231274.
［2］Harel D,Pnueli A. On the Development of Reactive Systems［J］. Logic and Model of

Concurrent Systems, 1984, 13:477498.
［3］Tretmans J. Test Generation with Inputs, Outputs and Repetitive Quiescence［J］. Software

Concepts and Tools, 1996, 17(3):103120.
［4］Tretmans J. Testing Concurrent Systems: A Formal Approach［C］∥Proc of CONCUR’99,

1999:4665.
［5］Tretmans J. Conformance Testing with Labelled Transition Systems: Implementation

Relations and Test Generation［J］.Computer Networks and ISDN Systems, 1996, 29(1):4979.
［6］Brinksma E,Tretmans J. Testing Transition Systems: An Annotated Bibliography［C］∥Proc

of MOVEP’00, 2001:187195.
［7］Latella D, Majzik I, Massink M. Towards a Formal Operational Semantics of UML Statechart

Diagrams［C］∥Proc of FMOODS’99,1999:331347.
［8］Latella D,Massink M. A Formal Testing Framework for UML Statechart Diagrams Behaviours:

From Theory to Automatic Verification［C］∥Proc of the 6th IEEE Int’l HighAssurance

Systems Engineering Symp,2001:1122.
［9］Latella D,Massink M. On Testing and Conformance Relations of UML Statechart Diagrams

Behaviours［C］∥Proc of the ACM SIGSOFT 2002 Int’l Symp on Software Testing and

Analysis,2002:144153.
［10］Gnesi S, Latella D, Massink M. Formal TestCase Generation for UML Statecharts［C］∥

Proc of ICECCS’04,2004:7584.
［11］Leveson N G, Heimdahl M P E,Hildreth H,et al. Requirements Specification for Process

Control Systems［J］. IEEE Transactions on Software Engineering, 1994, 20(9):684707.
［12］Selic B, Gullekson G, Ward P T. RealTime ObjectOriented Modeling［M］. John Wiley &

Sons, 1994.
［13］Booch G, Rumbaugh J, Jacobson I. The Unified Modeling Language User Guide［M］. Addison

Wesley, 1998.
［14］Harel D, Pnueli A, Schmidt J P, et al. On the Formal Semantics of Statecharts(Extended

Abstract)［C］∥Proc of Logic in Computer Science, 1987:5464.
［15］Harel D,Naamad A. The STATEMATE Semantics of Statecharts［J］. ACM Transactions on

Software Engineering Methodology, 1996, 5(4):293333.
［16］董威, 王戟, 齐治昌.UMLStatecharts的模型检验方法［J］. 软件学报, 2003, 14(4):750756.
［17］Bernot G. Testing Against Formal Specifications: A Theoretical View［C］∥Proc of

TAPSOFT’91,1991:99119.
［18］Tretmans J. A Formal Approach to Conformance Testing:［Ph D Thesis］［D］.University of

Twente (NL), 1992.