A Formal Testing Framework for UML Statecharts
Xuede Zhan · 2007
This paper introduces a method of formalizing syntax and semantics of UML statecharts with Z. According to this precise semantics, UML statecharts are transformed into FREE (flattened regular expression) state models. Proper testing pre-orders and equivalences are introduced which allow to equate/distinguish systems on the basis of their interaction with the surrounding environment, abstracting from their internal structure. The formal testing framework for UML statecharts is express with Z.