Le papier présente une technique de spécification et de validation empruntant les avantages de deux classes de méthodes de spécification, formelles et semi-formelles. Il s'inscrit dans le cadre d'intégration de méthodes pour la spécification des systèmes critiques Temps réels sûrs de fonctionnement. La technique que nous présentons utilise STATEMATE comme méthode semi -formelle et la logique temporelle FNLOG comme méthode formelle. La technique proposée présente une démarche d'intégration employant les notations de STATEMATE et de FNLOG. Elle définit des règles de transformation d'une spécification STATEMATE en des formules FNLOG et étend l'axiomatique de la logique temporelle FNLOG par de nouveaux lemmes pour prendre en compte les propriétés temporelles de durée. Le papier présente les différentes étapes de la démarche proposée, les règles de transformation ainsi que l'extension axiomatique.