Research on formal testing semantics for Statechart specification

This paper studies formal testing semantics for Statechart specification. In order to make the test cases generation process more simple and efficient, we propose testing semantics as a suitable semantics model for describing observable behavior subset of a Statechart specification, which is different from complete semantics used for Statechart specification verification and model checking. We first propose our Statechart notation, then mainly introduce three kinds of formal testing semantics - general semantics, critical semantics and real-time semantics, which go beyond semantics presented for formal verification. We also describe how to use this semantics model for not only general reactive systems, critical reactive systems but also real-time application reactive systems.