L'objectif principal de cette thèse est de proposer une approche efficace de modélisation et de résolution pour le problème d’ordonnancement, en mettant l’accent sur le partage multi-ressources et sur l’incertitude potentielle d’occurrence de certains événements. L'ordonnancement a pour objectif de réaliser un ensemble de tâches à la fois en respectant des contraintes prédéfinies et en optimisant le temps. Ce travail s’intéresse en particulier à la minimisation du temps total d’exécution. La plupart des approches existantes préconisent une modélisation mathématique exprimant des équations et des contraintes pour décrire et résoudre des problèmes d’ordonnancement. De telles démarches ont une complexité inhérente. Cependant dans l’industrie, la tâche de planification est récurrente et peut requérir des changements fréquents des contraintes. Outre cela, la prise en compte d’événements incertains est peu supportée par les approches existantes; cela peut toutefois augmenter la robustesse d’un ordonnancement. Pour répondre à ces problématiques, après une introduction, le chapitre 2 aborde le problème de l’ordonnancement à travers une démarche de modélisation visuelle, expressive et formelle, s’appuyant sur les automates pondérés et sur la théorie des automates temporisés. L’originalité des modèles proposés réside aussi dans leur capacité de décrire le partage de ressources multiples et proposer une approche de résolution efficace. Ces modèles ont l’avantage d’être directement exploitables par des outils de vérification formelle, à travers une démarche de preuve par contradiction vis-à-vis de l’existence d’une solution. Les résultats effectifs sont obtenus grâce à l’outil UPPAAL. La complexité inhérente à la production d’une solution optimale est abordée à travers un algorithme de recherche et d’amélioration itérative de solutions, offrant une complexité très prometteuse sur la classe de problèmes étudiés. Dans le chapitre 3, une composition synchrone est d’automates pondérés est proposée dans le but de résoudre le problème d’ordonnancement en effectuant une analyse d’atteignabilité optimale directement sur les modèles automates pondérés. Dans le quatrième chapitre, divers comportements incontrôlables tels que le temps de début, la durée de la tâche et l'occurrence d’échec dans un problème d‘ordonnancement sont modélisés par des automates de jeu temporisés. Ensuite, le problème est résolu en effectuant une synthèse de stratégie optimale dans le temps dans l'outil de synthèse TIGA. / The objective of scheduling problems is to find the optimal performing sequence for a set of tasks by respecting predefined constraints and optimizing a cost: time, energy, etc. Despite classical approaches, automata models are expressive and also robust against changes in the parameter setting and against changes in the problem specification. Besides, few studies have used formal verification approaches for addressing scheduling problems; yet none of them considered challenging and practical issues such as multi-resource sharing aspect, uncontrollable environment and reaching the optimal schedule in a reasonable time for industrializing the model. The main objective of this thesis is to propose an efficient modeling and solving approach for the scheduling problem, considering multi-resource sharing and potential uncertainty in occurrence of certain events. For this purpose, after an introduction in Chapter 1, Chapter 2 addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on weighted automata and the theory of timed automata. The originality of the proposed approach lies in ability of handling the sharing of multiple resources and proposing an efficient solving approach. The proposed models have the advantage of being directly exploitable by means of formal verification tools. The results are obtained using the UPPAAL tool. To solve the problem, an algorithm is developed based on iterating reachability analysis to obtain sub-optimal makespan. Results show the proposed model and solving approach provides a very promising complexity on the class of studied problems and can be applied to industrial cases. In Chapter 3, a synchronous composition of weighted automata is proposed to solve the scheduling problem by performing an optimal reachability analysis directly on the weighted automata models. In the fourth chapter, various uncontrollable behaviors such as the start time, the duration of the task and the failure occurrence in a scheduling problem are modeled by timed game automata. Then, the problem is solved by performing an optimal strategy synthesis over time in TIGA as a synthesis tool.

Cette thèse s'intéresse à la modélisation et à l'analyse dessystèmes temps-réel distribués.Un système distribué est constitué de plusieurs composantsqui évoluent de manière partiellement indépendante. Lorsque des actionsexécutables par différentscomposants sont indépendantes, elles sont dites concurrentes.Dans ce cas, elles peuvent être exécutées dans n'importe quel ordre, sanss'influencer, et l'état atteint après ces actions ne dépend pas de leur ordred'exécution.Dans les systèmes temps-réel distribués, les contraintes de temps créent desdépendances complexes entre les composants et les événements qui ont lieu surces composants. Malgré l'omniprésence et l'aspect critique de ces systèmes,beaucoup de leurs propriétés restent encore à étudier.En particulier, la nature distribuée de ces systèmes est souvent laissée de côté.Notre travail s'appuie sur deux formalismesde modélisation: les réseaux de Petri temporels et les réseaux d'automatestemporisés, et est divisé en deux parties.Dans la première partie, nous mettons en évidence les différences entre lessystèmes temporisés centralisés et les systèmes temporisés distribués. Nouscomparons les formalismes principaux et leurs extensions, avec une approcheoriginale qui considère la concurrence.En particulier, nous montrons comment transformer un réseau de Petri temporelen un réseau d'automates temporisés qui a le même comportement distribué.Nous nous intéressons ensuite aux horloges partagées dans lesréseaux d'automates temporisés. Les horloges partagées sont problématiqueslorsque l'on envisage d'implanter ces modèles sur des architecturesdistribuées. Nous montrons comment se passer des horloges partagées, touten préservant le comportement distribué, lorsque cela est possible.Dans la seconde partie, nous nous attachons à formaliser les dépendancesentre les événements dans les représentations en ordre partieldes exécutions des réseaux de Petri (temporels ou non).Les réseaux d'occurrence sont une de ces représentations, et leur structuredonne directement les relations de causalité, conflit et concurrence entreles événements. Cependant, nous montrons que, même dans le cas non temporisé,certaines relations logiques entre les événements nepeuvent pas être directement décrites par ces relations structurelles.Après avoir formalisé les relations logiques en question, nous résolvons leproblème de synthèse suivant: étant donnée une formule logique qui décrit unensemble d'exécutions, construire un réseau d'occurrence associé,quand celui-ci existe.Nous étudions ensuite les relations logiques dans un cadre temporisé simplifié,et montrons que le temps crée des dépendances complexes entre les événements.Ces dépendances peuvent être utilisées pour définir des dépliages canoniques deréseaux de Petri temporels, dans ce cadre simplifié. / This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.

Nous proposons dans cette thèse les approches de test pour la composition de services web. Nous nous intéressons aux test unitaire et d’intégration d’une orchestration de services web. L’aspect de vérification d’exécution en-ligne est aussi consideré. Nous définissons une plateforme de test unitaire pour l’orchestration de services web qui compose une architecture de test, une relation de conformité et deux approches de test basés sur le modèle de machine à l’états finis étendues temporisés: l’approche offline où les activités de test comme la génération de cas de test temporisé, l’exécution de test et l’assignement de verdict sont appliquées en séquentielle tandis que ces activités sont appliquées en parallèle dans l’approche online. Pour le test d’intégration d’une orchestration, nous combinons deux approches: active et passive.Au debut, l’approche active est utilisée pour activer une nouvelle session d’orchestration par l’envoi d’un message de requête SOAP. Après, tous les messages d’entré et de sortie de l’orchestration sont collectés et analysés par l’approche passive.Pour l’aspect de vérification d’exécution en-ligne, nous nous intéressons à la vérification d’une trace qui respecte un ensemble des constraintes, noté règles, ou pas. Nous avons proposé extendre le langage Nomad en définissant des constraintes sur chaque action atomique et un ensemble de corrélation de données entre les actions pour définir des règles pour le service web. Ce langage nous permet de définir des règles avec le temps futur et passé, et d’utiliser des opérations NOT, AND, OR pour combiner quelque conditions dans le contexte de la règle. Ensuite, nous proposons un algorithme pour vérifier l’exactitude d’une séquence des messages en parallèle avec le moteur de collecte de trace. / In this thesis, we propose the testing approaches for web service composition. We focus on unit, integrated testing of an orchestration of web services and also the runtime verification aspect. We defined an unit testing framework for an orchestration that is composed of a test architecture, a conformance relation and two proposed testing approaches based on Timed Extended Finite State Machine (TEFSM) model: offline which test activities as timed test case generation, test execution and verdict assignment are applied in sequential, and online which test activities are applied in parallel. For integrated testing of an orchestration, we combines of two approaches: active and passive. Firstly, active approach is used to start a new session of the orchestration by sending a SOAP request. Then all communicating messages among services are collected and analyzed by a passive approach. On the runtime verification aspect, we are interested in the correctness of an execution trace with a set of defined constraints, called rules. We have proposed to extend the Nomad language, by defining the constraints on each atomic action (fixed conditions) and a set of data correlations between the actions to define the rules for web services. This language allows us to define a rule with future and past time, and to use the operations: NOT, AND, OR to combines some conditions into a context of the rule. Afterwards, we proposed an algorithm to check correctness of a message sequence in parallel with the trace collection engine. Specifically, this algorithm verifies message by message without storing them.

Les travaux présentés dans ce manuscrit portent sur la conduite de systèmes complexes critiques. Ils s'inscrivent dans le cadre du projet CONNEXION (Investissements d'Avenir, BGLE2) qui réunit les principaux acteurs de la filière nucléaire française autour de la conception des systèmes de contrôle-commande des centrales et de leur exploitation. Dans le domaine de la conduite, les actions développées par le projet concernent la phase d'ingénierie avec pour objectif d'intégrer le point de vue de l'exploitant au plus tôt dans la validation des architectures de contrôle de commande, et la phase d'exploitation avec pour objectif de fournir une aide à la préparation et à l'exécution des procédures de conduite. Dans ce contexte, la contribution présentée dans ce mémoire porte sur la génération et la vérification de séquences d'actions de conduite répondant à un objectif donné et pouvant être opérées en toute sécurité sur le procédé. L'approche proposée repose la vérification d'une propriété d'atteignabilité sur un réseau d'automates temporisés modélisant le comportement des architectures. L'originalité réside dans la définition d’un cadre formel de modélisation sous la forme de patrons favorisant la réutilisabilité des modèles ainsi que dans la proposition d'algorithmes d'abstraction et de recherche d'atteignabilité itératifs exploitant la hiérarchisation intrinsèque des architectures afin de permettre le passage à l'échelle de l'approche proposée. La contribution a été éprouvée sur la plate-forme d'expérimentation CISPI du CRAN puis sur un cas d'étude à échelle industrielle proposé dans le cadre du projet CONNEXION / The works presented in this manuscript deals with critical complex systems operation. They are part of the CONNEXION project (Investissements d'Avenir, BGLE2), which involves the main actors in the French nuclear industry around the design of control systems for power plants and their operation. In the operation field, the actions developed by the project concern the engineering phase with the aim of integrating the operator's point of view as soon as possible in the validation of control architectures, and the operation phase with the aim of providing assistance in the preparation and execution of operation procedures. In this context, the contribution presented in this manuscript deals with the generation and verification of action sequences that meet a given objective and that can be safely operated on the process. The proposed approach relies on verifying a reachability property on a network of timed automata modelling the behavior of architectures. The originality is in the definition of a formal modelling framework using patterns promoting the reusability of models, as well as in the proposition of abstraction and reachability iterative analysis algorithms exploiting the intrinsic hierarchization of architectures in order to scale-up of the proposed approach. The contribution was evaluated on the CISPI experimental platform of the CRAN, and on an industrial scale case study proposed within the framework of the CONNEXION project

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.

Les travaux présentés dans cette thèse portent sur l'ordonnancement d'applications sur des plate- formes hétérogènes à grande échelle. Dans la mesure où le problème général est trop complexe pour être résolu de façon exacte, nous considérons deux relaxations. Tâches divisibles : La première partie est consacrée aux tâches divisibles, qui sont des appli- cations parfaitement parallèles et pouvant être arbitrairement subdivisées pour être réparties sur de nombreux processeurs. Nous cherchons à minimiser le temps de travail total lors de l'exécution de plusieurs applications aux caractéristiques différentes sur un réseau linéaire de processeurs, sachant que les données peuvent être distribuées en plusieurs tournées. Le nombre de ces tour- nées étant fixé, nous décrivons un algorithme optimal pour déterminer précisément ces tournées, et nous montrons que toute solution optimale requiert un nombre infini de tournées, résultat restant vrai sur des plate-formes non plus linéaires mais en étoile. Nous comparons également notre méthode à des méthodes déjà existantes. Ordonnancement en régime permanent : La seconde partie s'attache à l'ordonnancement de nombreuses copies du même graphe de tâches représentant une application donnée. Au lieu de chercher à minimiser le temps de travail total, nous optimisons uniquement le cœur de l'or- donnancement. Tout d'abord, nous étudions des ordonnancements cycliques de ces applications sur des plate-formes hétérogènes, basés sur une seule allocation pour faciliter leur utilisation. Ce problème étant NP-complet, nous donnons non seulement un algorithme optimal, mais éga- lement différentes heuristiques permettant d'obtenir rapidement des ordonnancements efficaces. Nous les comparons à ces méthodes classiques d'ordonnancement, telles que HEFT. Dans un second temps, nous étudions des applications plus simples, faites de nombreuses tâches indépendantes, que l'on veut exécuter sur une plate-forme en étoile. Les caractéristiques de ces tâches variant, nous supposons qu'elles peuvent être modélisées par des variables aléatoires. Cela nous permet de proposer une ε-approximation dans un cadre clairvoyant, alors que l'ordonnan- ceur dispose de toutes les informations nécessaires. Nous exposons également des heuristiques dans un cadre non-clairvoyant. Ces différentes méthodes montrent que malgré la dynamicité des tâches, il reste intéressant d'utiliser un ordonnancement statique et non des stratégies plus dynamiques comme On-Demand. Nous nous intéressons ensuite à des applications, dont plusieurs tâches sont répliquées sur plu- sieurs processeurs de la plate-forme de calcul afin d'améliorer le débit total. Dans ce cas, même si les différentes instances sont distribuées aux processeurs tour à tour, le calcul du débit est difficile. Modélisant le problème par des réseaux de Petri temporisés, nous montrons comment le calculer, prouvant également que ce calcul peut être fait en temps polynomial avec le modèle Strict One-Port. Enfin, le dernier chapitre est consacré à l'application de ces techniques à un processeur multi- cœur hétérogène, le Cell d'IBM. Nous présentons donc un modèle théorique de ce processeur ainsi qu'un algorithme d'ordonnancement adapté. Une implémentation réelle de cet ordonnanceur a été effectuée, permettant d'obtenir des débits intéressants tout en simplifiant l'utilisation de ce processeur et validant notre modèle théorique.

L'objet des travaux de cette thèse est de proposer de nouveaux processus de définition de tests (testabilité), de nouvelles méthodes de tests, ainsi que de nouvelles méthodes d'interprétation des tests (diagnostic). Ces travaux ont été menés dans le cadre de l'aéronautique et ont porté dans un premier temps sur l'identification des besoins en diagnostic des hélicoptères. Les problématiques liées au test et au diagnostic des hélicoptères portaient sur : - La non-détection de certaines défaillances - L'occurrence de nombreuses fausses alarmes - L'ambiguïté de localisation de défaillances Dans un premier temps nous avons réalisé l'état de l'art des recherches en diagnostic, ceci afin de sélectionner les technologies et méthodologies permettant de répondre aux problématiques identifiées. Les technologies candidates ont ensuite été architecturées afin de proposer un traitement intégré permettant de répondre à l'ensemble des besoins identifiés. Ainsi nous avons travaillé sur les méthodologies de définition du test, aux moyens d'outils de simulation de la testabilité. Nous avons aussi défini de nouvelles méthodes de test permettant de déterminer l'état de capteurs analogiques aux moyens d'algorithmes basés sur des évaluateurs de calcul de variation de l'écart type, du facteur de forme et du rapport signal sur bruit. Nous avons ensuite travaillé sur l'amélioration du diagnostic au niveau système à l'aide d'automates temporisés afin de simuler le fonctionnement des arbres de tests élémentaires. Ces travaux ont ensuite conduit à la modélisation et au diagnostic des systèmes complexes à l'aide des diagrammes d'état, des arbres de défaillances dynamiques, ainsi que leur simulation à l'aide des réseaux de Petri. Les modèles utilisés ont été complétés au moyen de nouvelles portes dynamiques. Ces travaux ont été appliqués au monde aéronautique, sur plusieurs hélicoptères et ont fait l'objet de deux brevets.

Les systèmes de commande en réseau (SCR) sont de plus en plus répandus dans le milieu industriel. Ils procurent en effet de nombreux avantages en termes de coût, de flexibilité, de maintenance, etc. Cependant,l’introduction d’un réseau, qui par nature est composé de ressources partagées, impacte considérablement les performances temporelles des systèmes de commande. Un signal de commande par exemple n’arrive à destination qu’après un certain délai. Pour s’assurer que ce délai soit inférieur à un certain seuil de sécurité ou du respect d’autres contraintes temps réels de ces systèmes, une évaluation au préalable, avant la mise en service d’un SCR, s’avère donc nécessaire. Dans nos travaux de recherche, nous nous intéressons à la réactivité des SCR client/serveur et évaluons leur temps de réponse.Notre contribution dans ces travaux est d’adopter une approche analytique à base de l’algèbre (Max,+) et remédier aux problèmes des méthodes existantes comme l’explosion combinatoire de la vérification formelle ou de la non exhaustivité des approches par simulation. Après modélisation des SCR client/serveur à l’aide de Graphe d’Evénements Temporisés puis représentation de leurs dynamiques à l’aides d’équations (Max,+) linéaires, nous obtenons des formules de calcul direct du temps de réponse. Plus précisément, nous adoptons une analyse déterministe pour calculer les bornes, minimale et maximale, du temps de réponse puis une analyse stochastique pour calculer la fonction de sa distribution. De plus, nous prenons en compte dans nos travaux tous les délais élémentaires qui composent le temps de réponse, y compris les délais de bout-en-bout, dus à la traversée du seul réseau de communication. Ce dernier étant naturellement composé de ressources partagées, rendant l’utilisation des modèles (Max,+) classiques impossibles, nous introduisons une nouvelle approche de modélisation à base du formalisme (Max,+) mais prenant en compte le concept de conflit ou ressource partagée.L’exemple d’un réseau de type Ethernet est considéré pour évaluer ces délais de bout-en-bout. Par ailleurs, cette nouvelle méthode (Max,+) est assez générique et reste applicable à de nombreux systèmes impliquant des ressources partagées, au delà des seuls réseaux de communication. Enfin, pour vérifier la validité des résultats obtenus dans nos travaux, notamment la formule de la borne maximale du temps de réponse, une compagne de mesures expérimentales sont menées sur une plateforme dédiée. Différentes configurations et conditions de trafic dans un réseau Ethernet sont considérées. / Networked automation systems (NAS) are more and more used in industry, given the several advantages they provide like flexibility, low cost, ease of maintenance, etc. However, the use of a communication network in SCR means in essence sharing some resources and therefore strikingly impacts their time performances. For instance, a control signal does get to its destination (actuator) only after a non zero delay. So, to guarantee that such a delay is shorter than a given threshold or other time constraints well respected, an a priori evaluation is necessary before operating the SCR. In our research activities, we are interested in client/server SCR reactivity and the evaluation of their response time.Our contribution in this investigation is the introduction of a (Max,+) Algebra-based analytic approach to solve some problems, faced in the existing methods like state explosion of model checking or the non exhaustivity of simulation. So, after getting Timed Event Graphs based models of the SCR and their linear state (Max,+) representation, we obtain formulae that enables to calculate straightforwardly the SCR response times. More precisely, we obtain formulae of the bounds of response time by adopting a deterministic analysis and other formulae to calculate the probability density of response time by considering a stochastic analysis. Moreover, in our investigation we take into account every single elementary delay involved in the response time, including the end-to-end delays, due exclusively to crossing the communication network. This latter being however constituted of shared resources, making by the way the use of TEG and (Max,+) Algebra impossible, we introduce a novel approach to model the communication network. This approach brings to life a new class of Petri nets, called Conflicting Timed Event Graphs (CTEG), which enables us to solve the problem of the shared resources. We also manage to represent the CTEG dynamics using recurrent (Max,+) equations and therefore calculate the end to-end delays. An Ethernet-based network is studied as an example to apply this novel approach. Note by the way that the field of application of this approach borders largely communication networks and is quite possible when dealing with other systems.Finally, to validate the different results of our research activities and the related hypotheses, especially the maximal bound of response time formula, we carry out lots of experimental measurements on a lab facility. We compare the measures to the formula predictions and check their agreement under different conditions.

La conception des systèmes de contrôle-commande souffre souvent des problèmes de communication et d’interprétation des spécifications entre les différents intervenants provenant souvent de domaines techniques très variés. Afin de cadrer la conception de ces systèmes, plusieurs démarches ont été proposées dans la littérature. Parmi elles, la démarche dite mixte (ascendante/descendante), qui voit la conception réalisée en deux phases. Dans la première phase (ascendante), un modèle du système est défini à partir d’un ensemble de composants standardisés. Ce modèle subit, dans la deuxième phase (descendante), plusieurs raffinages et transformations pour obtenir des modèles plus concrets (codes,applicatifs, etc.). Afin de garantir la qualité des systèmes conçus par cette démarche, nous proposons dans cette thèse, deux approches de vérification formelle basées sur le Model-Checking. La première approche porte sur la vérification des composants standardisés et permet la vérification d’une chaîne de contrôle-commande élémentaire complète. La deuxième approche consiste en la vérification des modèles d’architecture (P&ID) utilisés pour la génération des programmes de contrôle-commande. Cette dernière est basée sur la définition d’un style architectural en Alloy pour la norme ANSI/ISA-5.1. Pour supporter les deux approches, deux flots de vérification formelle semi-automatisés basés sur les concepts de l’IDM ont été proposés. L’intégration des méthodes formelles dans un contexte industriel est facilitée, ainsi, par la génération automatique des modèles formels à partir des modèles de conception maîtrisés par les concepteurs métiers. Nos deux approches ont été validées sur un cas industriel concret concernant un système de gestion de fluide embarqué dans un navire. / The design of control-command systems often suffers from problems of communication and interpretation of specifications between the various designers, frequently coming from a wide range of technical fields. In order to address the design of these systems, several methods have been proposed in the literature. Among them, the so-called mixed method (bottom-up/top-down), which sees the design realized in two steps. In the first step (bottom-up), a model of the system is defined from a set of standardized components. This model undergoes, in the second (top-down) step, several refinements and transformations to obtain more concrete models (codes, applications, etc.). To guarantee the quality of the systems designed according to this method, we propose two formal verification approaches,based on Model-Checking, in this thesis. The first approach concerns the verification of standardized components and allows the verification of a complete elementary control-command chain. The second one consists in verifying the model of architecture (P&ID) used for the generation of control programs.The latter is based on the definition of an architectural style in Alloy for the ANSI/ISA-5.1 standard. To support both approaches, two formal semi-automated verification flows based on Model-Driven Engineering have been proposed. This integration of formal methods in an industrial context is facilitated by the automatic generation of formal models from design models carried out by business designers. Our two approaches have been validated on a concrete industrial case of a fluid management system embedded in a ship.

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.