Dans le domaine des systèmes informatisés où la fiabilité est la première priorité, les méthodes formelles ont prouvé leur efficacité pour la conception de logiciels sûrs. La dépendance à de tels systèmes augmente, et les contraintes rencontrées se font plus diverses et précises, en particulier les contraintes temporelles. Certaines méthodes formelles, notamment la méthode B, rendent la conception malaisée sous de telles contraintes, puisqu'elles n'ont pas été prévues pour cela à l'origine.<br /><br />Nous nous proposons donc d'étendre la méthode B pour lui permettre de spécifier et valider des systèmes à contraintes temporelles complexes. Nous utilisons pour ce faire des calculs de durées pour exprimer la sémantique du langage B et en déduire une extension conservative qui permet de l'utiliser à la fois dans son cadre d'origine et dans le cadre de systèmes à contraintes temporelles.<br /><br />Nous nous penchons également sur le problème de l'utilisation d'un outil de preuve générique pour valider des formules de calcul des durées. La généricité de ce type d'outil répond à la multiplication des méthodes formelles, mais pose le problème de l'intégration des fondations mathématiques de ces méthodes à un outil générique. Nous proposons donc d'étudier la mise en oeuvre en plongement léger du calcul des durées dans l'assistant de preuve Coq. Nous en déduisons un retour sur expérience de la définition d'une logique modale particulière dans un outil à vocation générique.