Spécification et vérification d'un ordonnanceur en B via les automates temporisés