Nous nous intéressons aux étapes de recueil des besoins et de spécification d'une application de téléréhabilitation de patients atteints de maladies chroniques respiratoires. Après avoir réalisé des entretiens avec les experts impliqués dans la définition des processus de réhabilitation, un cahier des charges a été établi sous forme textuelle et sous forme de modèles UML. Nous avons constaté que la modélisation UML est un réel apport pour la maîtrise d'ouvrage mais elle doit être accompagnée d'une étape de modélisation formelle et de vérification pour analyser les processus et vérifier des propriétés. Ici nous nous concentrons sur les propriétés de vivacité et de sûreté. Nous avons choisi U PPAAL comme outil de simulation et de vérification formelle. Nous montrons sur cette étude de cas quels sont les apports de chacune des étapes de modélisation informelle et formelle pour toutes les parties prenantes du projet.