ISBN-13: 9786131534706 / Francuski / Miękka / 2018 / 204 str.
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."
Cet ouvrage sintéresse à la conception de systèmes temps-réel en sappuyant sur la méthode formelle RT-Lotos, extension temporelle à lalgèbre de processus Lotos. Il aborde plusieurs points relatifs à la spécification, la validation et lordonnancement 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 daccessibilité. La deuxième partie étudie la notion de cohérence temporelle et propose une technique basée sur lanalyse du graphe des régions ainsi quun 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 sappuyant sur RT-Lotos. Ainsi, nous définissons une méthodologie qui sinscrit dans les techniques de développement industriel classiques et qui permet une vérification formelle de systèmes temps-réel.