On semantics and refinement of UML statecharts: A coalgebraic view

On semantics and refinement of UML statecharts: A coalgebraic view (link)
M. Sun, Z. Naixiao and L. S. Barbosa. In Cuellar, J. and Liu, Z., editors, Proc. of 2nd IEEE Int. Conf. on Software Engineering and Formal Methods, Beijing, IEEE Computer Society Press, pp 164--173, September, 2004.

Abstract

Statecharts was conceived as a visual formalism for the design of reactive systems. UML statecharts is an object-based variant of classical statecharts, incorporating several concepts different from the classical statecharts. This paper discusses a coalgebraic description of UML statecharts, directly derived from its operational semantics. In particular, such an approach induces suitable notions of equivalence and (behavioral) refinement for statecharts. Finally, a few refinement laws are investigated to support verifiable step-wise system development with statecharts.