Plusieurs outils ont été développés pour la vérification des systèmes temporisés, par exemple COSPAN, HyTech, KRONOS, RT-Spin... Dans cet exposé, nous présentons la boite à outils UPPAAL développée conjointement par l'Université d'Uppsala et l'Université d'Aalborg. Nous survolons les aspects modélisation, simulation et vérification de point de vue pratique (en considérant la modélisation du protocole de choix d'un leader dans IEEE 1394) et de point de vue théorique (en présentant les structures de données et les algorithmes utilisés). Nous considérons la variante paramétrée du protocole IEEE 1394 pour illustrer les limites de UPPAAL et de HyTech et pour donner une motivation de nos travaux dans cette direction.