Colin F. Snook, Marina Waldén: Refinement of Statemachines Using Event B Semantics. B 2007: 171-185