Modélisation polychrone et évaluation de systèmes temps réel

Real-time systems are devices consisting of hardware and software with functional and timing constraints for the interaction with their environment. Telecommunication, nuclear power plants, avionics, and medical technology are typical domains where such systems are encountered. These systems are often critical because of the high human and economic stakes. Therefore, the development of these systems requires highly reliable methods. The synchronous approach has been proposed in order to answer this demand. Its mathematical basis provides a formal framework that favors the description and validation of real-time systems. The multi clock or polychronous model stands out from other synchronous speci cation models by the fact that it allows the description of systems where each component can have its own activation clock. Besides formal validation, it favors component-based approaches and modular development of large-scale systems. This document suggests a methodology for the design of real-time systems that uses as formalism the synchronous language Signal which relies on the polychronous model. It uses the formal tools and techniques based on this model in order to verify both behavioral and non functional properties. This facilitates design space exploration. The methodology presented here allows to design systems that contain asynchronous mechanisms using the synchronous approach. It illustrates the characterization of real-time behaviors in the polychronous model. Avionics is considered as privileged application domain in the current document. This work has been supported by the european project SafeAir (Advanced Design Tools for Aircraft Systems and Airborne Software) in which many industrials are involved. We especially are interested in the design of applications following the Integrated Modular Avionics (IMA) architecture model that is based on the avionic standard ARINC. This leads to the implementation of a library in Signal containing real-time executive services de fined by ARINC.Les systemes temps reel sont des dispositifs constitues de materiels et de logiciels soumis a des contraintes a la fois fonctionnelles et temporelles pour realiser des traitements, et agir sur leur environnement. Des exemples de domaines o u on rencontre de tels systemes sont les telecommunications, le nucl eaire, l'avionique ou le medical. Ces systemes sont souvent critiques a cause d'enjeux humains et economiques importants. Leur developpement exige donc des methodes tres ables. L'approche synchrone a et e proposee dans le but de repondre a cette attente. Ses fondements mathematiques o rent un cadre formel propice a la description et la validation des systemes temps reel. Parmi les modeles de specification synchrone, le modele multi-horloge ou polychrone se distingue par le fait qu'il permet de decrire des systemes o u chaque composant peut avoir sa propre horloge d'activation. Outre la validation formelle, il favorise des approches orientees composants et le d eveloppement modulaire de systemes a grande echelle. Cette these propose une m ethodologie de conception de syst emes temps reel en utilisant comme formalisme de description le langage synchrone Signal fond e sur le mod ele polychrone. Elle utilise les outils et techniques formels bas es sur ce modele pour verifier des proprietes comportementales portant sur des aspects tant fonctionnels que non fonctionnels. Cette demarche facilite l' evaluation des choix de conception. La methodologie propos ee permet de concevoir des systemes comportant des m ecanismes asynchrones a l'aide de l'approche synchrone. Elle illustre la caracterisation de comportements temps r eel dans le modele polychrone. L'avionique est le domaine d'application privilegie par la these. Cette derniere s'inscrit dans le cadre du projet europ een IST SafeAir (Advanced Design Tools for Aircraft Systems and Airborne Software), regroupant plusieurs industriels. Nous nous sommes particulierement interesses a la conception d'applications suivant le mod ele d'architecture IMA (Integrated Modular Avionics) sur lequel repose la norme avionique ARINC. Cela a conduit a la r ealisation d'une bibliotheque Signal de composants, constituee en majeure partie de services d'un ex ecutif temps reel d e nis par ARINC