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