Cet ouvrage s'interesse a la conception de systemes temps-reel en s'appuyant sur la methode formelle RT-Lotos, extension temporelle a l'algebre de processus Lotos. Il aborde plusieurs points relatifs a la specification, la validation et l'ordonnancement de systemes concurrents sujets a des contraintes logiques et temporelles. La premiere partie presente le langage RT-Lotos et la technique de verification formelle associee basee sur une analyse d'accessibilite. La deuxieme partie etudie la notion de coherence temporelle et propose une technique basee sur l'analyse du graphe des regions ainsi qu'un modele formel pour exploiter sous un nouvel angle des informations issues de la verification formelle. Enfin, la troisieme partie se penche sur les liens possibles entre methodes formelles et semi-formelles. Dans ce cadre, nous proposons une semantique formelle pour les diagrammes UML s'appuyant sur RT-Lotos. Ainsi, nous definissons une methodologie qui s'inscrit dans les techniques de developpement industriel classiques et qui permet une verification formelle de systemes temps-reel."