Pour faciliter la phase de spécification, nous présentons un débogueur multivers pour les machines à état UML ainsi que deux extensions à cette approche : Les breakpoints temporels permettent l'utilisation de multiples logiques temporelles pour explorer le modèle. La réduction permet un certain contrôle sur l'espace d'état exploré pour permettre le passage à l'échelle.