Xuede Zhan, Huaikou Miao: An Approach to Formalizing the Semantics of UML Statecharts. ER 2004: 753-765