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...