Validation d'un modèle basée sur les RdPT pour la spécification et l'analyse des systèmes temps réel complexes : Application aux systèmes multimédias

Nowadays, parallel systems are more and more used in the computing world. ; they are characterized by their power and complexity. An important class of computing systems is that of real-time systems.Real-time systems are systems whose behavior must satisfy hard time constraints. They are generally characterized by complex interactions with their environment; they must therefore necessarily be reliable. This includes highly reactive systems whose decisions can have immediate and irreversible consequences on goods and men. Their fields of application are wide, ranging from domestic applications such as household heating and cooking control systems, to the most complex and critical systems such as avionics control systems, nuclear, industry and telecommunications.To verify the reliability of such systems, formal methods have been widely considered and stand an important step in their development process. It starts with the proposal of a mathematical model capable of faithfully describing their temporal behavior and follows the proposal of analysis techniques adapted to this model, allowing to verify the qualitative and quantitative properties of these systems.Subsequently, the subject of our work is to design a framework related to the specification and to the verification of multimedia applications whose complex requirements partly take up the needs of real-time systems. The proposals that we develop in this thesis could resonate with real-time applications in the broad sense, due to the fact that they allow to define a unified formal framework allowing the management of a large part of theissues raised in such systems.De nos jours, les systèmes parallèles sont de plus en plus répandus dans le monde informatique ; ils sont caractérisés par leur puissance et leur complexité. Une classe importante des systèmes informatiques est celle des systèmes temps réel.Les systèmes temps réel sont des systèmes dont le comportement doit satisfaire des contraintes temporelles strictes. Ils sont en général caractérisés par des interactions complexes avec l'environnement ; ils doivent par conséquent nécessairement être fiables. Il comprennent les systèmes hautement réactifs dont les décisions peuvent avoir des conséquences immédiates et irréversibles sur des biens et des hommes. Leurs domaines d'application est large, allant de la simple utilisation domestique tels que les systèmes de contrôle des chauffages et des cuisinières, jusqu'aux systèmes les plus complexes et les plus critiques tels que les systèmes de commande de l'avionique, le nucléaire, l'industrie et les télécommunications. Pour vérifier la fiabilité de tels systèmes, les méthodes formelles ont été largement utilisées et constituent une étape importante dans leur processus d'élaboration. Cela commence par la proposition d'un modèle mathématique capable de d'écrire fidèlement leurs comportements temporels et s'en suit la proposition de techniques d'analyse adaptées ç ce modèle, permettant de vérifier qualitativement et quantitativement les propriétés de ces systèmes.Par la suite, nous inscrivons notre travail dans un cadre particulier relatif à la spécification et à la vérification des applications multimédias dont les exigences complexes résument en partie les besoins des systèmes temps réel. Les propositions que nous développons dans cette thèsepourraient trouver écho au près des applications temps réel au sens large, du fait qu'elles permettent de définir un cadre formel unifié permettant la prise en charge d'une grande partie des problématiques posées dans ce type de systèmes