Requirements Engineering for Reactive Systems: Coloured Petri Nets for an Elevator Controller