A Petri-net approach to refining object behavioural specifications