Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-Lotos

Rapporteurs : Richard Castanet Elie Najm Examinateurs : Michel Diaz Hubert Garavel Patrick Sallé François VernadatThis thesis deals with the design of real-time systems based on the RT-Lotos formal method, a timed extension to the Lotos process algebra. It addresses several issues related to the specification, validation and scheduling of concurrent systems subject to logical and temporal constraints. The first part of the work proposes a review of formal methods for the specification and validation of real-time systems. It also presents the RT-Lotos language and the associated formal verification technique based on reachability analysis. Finally, it details some works based on the timed automaton (called a DTA) derived from an RT-Lotos specification in order to carry out fast simulations, and to interface with model-checking tools. The second part presents a study on the concept of temporal consistency and proposes both a technique and a formal model to exploit in a new way the information resulting from the formal reachability analysis. This approach proposes to refine the regions graph, to remove paths considered to be nondesirable, to extract the firing instants of the actions, and to present this information in a new model of timed automaton (called a TLSA) which is able to schedule the execution of the actions of a system. Finally, the third part considers the possible relations between formal and nonformal methods. Within this framework, we propose a formal semantics for UML diagrams, after having defined a real-time extension to UML (called TURTLE). Thus, we define a methodology, which takes place inside traditional industrial development techniques and which allows a formal analysis of real-time systems.Ce mémoire de thèse 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 propose un éventail de méthodes formelles pour la spécification et la validation de systèmes temps-réel. Elle présente également le langage RT-Lotos et la technique de vérification formelle associée basée sur une analyse d'accessibilité. Elle détaille finalement un ensemble de travaux concernant l'automate temporisé (appelé un DTA) dérivé d'une spécification RT-Lotos, avec comme objectifs d'exécuter des simulations rapides, et de s'interfacer avec des outils de vérification de type model-checker. La deuxième partie présente une étude sur la notion de cohérence temporelle et propose une technique ainsi qu'un modèle formel pour exploiter sous un nouvel angle des informations issues de la vérification formelle par analyse d'accessibilité. Cette approche propose de raffiner le graphe des régions, d'en élaguer certaines branches jugées non souhaitables, d'extraire les dates de tir possible des actions, et de présenter ces informations sous la forme d'un nouveau type d'automate temporisé (appelé un TLSA) ayant pour vocation l'ordonnancement dans le temps des actions d'un système. 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, après avoir défini une extension temps-réel à UML (appelée TURTLE). 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