Ce travail s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif de la thèse est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles.<br />Deux extensions du langage sont proposées : une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel. <br />Une étude formelle complète a été menée sur la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et des moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire le modèle sans sous composant.<br />Enfin, le langage temporisé est implanté dans un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé. Ainsi, certains systèmes réels ont pu être modélisés puis des propriétés ont été vérifiées à l'aide du model checker UPPAAL.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

Notre travail de recherche concerne l'étude du diagnostic à base de modèles pour les systèmes temporisés et pour une sous-classe de systèmes dynamiques hybrides. Nous avons d'abord développé une méthode de diagnostic basée sur la compilation hors-ligne d'un diagnostiqueur à partir du modèle automate temporisé du système à diagnostiquer. Une méthode systématique permettant la vérification de la diagnosticabilité du modèle utilisé est ensuite donnée. Nous avons ensuite proposé une méthode de diagnostic pour une sous-classe de systèmes dynamiques hybrides modélisés par des automates hybrides rectangulaires. Cette méthode repose sur l'utilisation d'une procédure de diagnostic en-ligne qui estime l'état courant du système ainsi que les occurrences des défauts non-observables. Enfin, nous avons proposé une méthode de vérification de la diagnosticabilité du langage temporisé accepté par un automate hybride rectangulaire vérifiant les hypothèses considérées dans notre travail.

La composition des systèmes temporisés est source de nombreux problèmes, notamment de blocage. Nous proposons un cadre de description compositionnelle des systèmes temporisés qui préserve la réactivité temprorelle, à savoir que si le système ne peut réagir, alors le temps peut avancer. Nous effectuons d'abord une étude préliminaire sur la spécification des évolutions temporelles dans les systèmes, débouchant sur la définition de mécanismes de description adéquats. Ceci nous permet de définir une classe de modèles temporisés temporellement réactifs, par construction. Nous définissons sur cette classe des opérateurs de choix et de composition parallèle qui préservent cette propriété. En outre, les opérateurs sont définis de sorte à préserver l'activité dans le sens où si à partir d'un état une action est possible dans un composant, alors une action est possible dans la composition. L'opérateur de composition parallèle respecte également la propriété de progrès maximal grâce à l'utilisation d'opérateurs de choix avec priorités qui favorise les synchronisations. Un cadre général est donné pour exprimer différents modes de synchronisation, parmi lesquels on retiendra AND (synchronisation classique), MAX (synchronisation avec attente) et MIN (interruption). Pour terminer, nous développons une approche algébrique pour une sous-classe des modèles considérés.

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. / Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.

Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système décrit par un transducteur. Malgré les limites imposées par ce modèle, nous montrons que le problème de synthèse est indécidable en général. Cependant, lorsque le système est fonctionnel, c'est-à-dire que son fonctionnement externe est toujours le même, le problème devient décidable. Nous généralisons ensuite le concept d'opacité aux systèmes probabilistes, en donnant des mesures groupées en deux familles. Lorsque le système est opaque, nous évaluons la robustesse de cette opacité vis-à-vis des informations données par les lois de probabilités du système. Lorsque le système n'est pas opaque, nous évaluons la taille de la faille de sécurité induite par cette non opacité. Enfin, nous étudions le modèle des automates temporisés à interruptions (ITA) où les informations sur l'écoulement du temps sont organisées en niveaux comparables à des niveaux d'accréditation. Nous étudions les propriétés de régularité et de clôture des langages temporisés générés par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisées.