Cet ouvrage s'int resse la conception de syst mes temps-r el en s'appuyant sur la m thode formelle RT-Lotos, extension temporelle l'alg bre de processus Lotos. Il aborde plusieurs points relatifs la sp cification, la validation et l'ordonnancement de syst mes concurrents sujets des contraintes logiques et temporelles. La premi re partie pr sente le langage RT-Lotos et la technique de v rification formelle associ e bas e sur une analyse d'accessibilit . La deuxi me partie tudie la notion de coh rence temporelle et propose une technique bas e sur l'analyse du graphe des r gions ainsi qu'un mod le formel pour exploiter sous un nouvel angle des informations issues de la v rification formelle. Enfin, la troisi me partie se penche sur les liens possibles entre m thodes formelles et semi-formelles. Dans ce cadre, nous proposons une s mantique formelle pour les diagrammes UML s'appuyant sur RT-Lotos. Ainsi, nous d finissons une m thodologie qui s'inscrit dans les techniques de d veloppement industriel classiques et qui permet une v rification formelle de syst mes temps-r el.