Computing Refactorings of Behavior Models

Abstract. For given behavior models expressed in statechart-like for-malisms, we show how to compute semantically equivalent but struc-turally dierent models. These refactorings are dened by user-provided logical predicates that partition the system's state space and that char-acterize coherent parts|modes or control states|of the behavior.