Francouzština
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.
