L'objet de cette thèse concerne les propriétés du groupe symétrique à travers deux problèmes. Le premier consiste à étudier l'action du groupe symétrique sur la fraction (...). En appliquant certaines opérations sur les graphes et les cartes, nous donnons des algorithmes et des formules combinatoires pour déterminer complètement la fraction réduite suivante : (...). L'auteur C. Greene a introduit cette fraction rationnelle pour généraliser des identités liées a la règle de Murnaghan-Nakayama. Nous utilisons (...) pour établir un nouvel algorithme de décomposition en éléments simples à l'aide des graphes. Dans la seconde partie, nous cherchons a développer les puissances paires du Vandermonde au moyen de fonctions symétriques. En particulier, nous proposons une écriture hyperdéterminantale des coefficients du développement des puissances paires du Vandermonde dans la base des fonctions de Schur. Nous obtenons plusieurs identités reliant les puissances paires du Vandermonde et les polynômes de Jack. Puis nous introduisons une q-déformation des puissances paires du Vandermonde que nous exprimons grâce aux polynômes de Macdonald

Cette thèse, à caractère industriel, vise à répondre à une problématique de production de l’entreprise ITK. Par la mise en oeuvre des techniques de l’ingénierie dirigée par les modèles, nous proposons un environnement de modélisation et de simulation pour la croissance des plantes. Outre sa facilité d’utilisation pour les agronomes, le prototype obtenu permet la génération automatique de code Java des modèles à intégrer dans des outils d’aide à la décision exécutés sur une plateforme Java Enterprise Edition. / This PhD thesis has an industrial purpose. It is motivated by a software production issue met within the ITK company. Using the techniques provided by model-driven engineering, we propose a modeling and simulation environment dedicated to plant growth. The prototype achieved proves to be easy to use for crop modelers. It is also enhanced with a Java code generation feature. The models obtained from this code generation are designed to be integrated into decision support systems running on a Java Entreprise Edition platform.

Ce travail de thèse constitue le prolongement direct des travaux de thèse Chachuat (2001) sur l'optimisation dynamique et la commande optimale des stations de traitement de petite taille. L'objectif est d'aller plus loin en s'intéressant aux dimensionnement et fonctionnement optimaux des stations de traitement des eaux usées de toute taille. Ainsi, dans une première étape, l'optimisation des stations de traitement de petite taille a été abordée. Contrairement à ce qui a été fait jusqu'à maintenant : (i) l'aération n'est plus alternée, mais continue, (ii) le décanteur n'est plus considéré comme parfait, mais son fonctionnement est modélisé à l'aide d'une série de 10 couches de décantation, (iii) la méthode d'optimisation développée est fondée sur la méthode des sensibilités implémentée au sein du logiciel de simulation et optimisation dynamiques gProms, utilisé dans toute la thèse. L'influence du modèle du décanteur sur la minimisation de l'énergie d'aération a été particulièrement analysée. Dans une deuxième étape, les stations de traitement de grande taille sont considérées. Plus spécifiquement, le modèle benchmark développé par le réseau européen COST a été utilisé pour décrire leur fonctionnement. Un « foreignobject » a été développé pour que la simulation et l'optimisation du fonctionnement de ces stations soient possibles sous gProms. L'optimisation a notamment montré que la consommation d'énergie d'aération pouvait être réduite d'au moins de 30% par rapport au fonctionnement actuel de ces stations. Dans une troisième étape, l'optimisation du dimensionnement des stations de traitement de grande taille a été étudiée. Une superstructure a ainsi été définie avec plusieurs (cinq) réacteurs et un décanteur. Toutes les possibilités de recyclage et de court-circuit entre les réacteurs d'une part et entre les réacteurs et le décanteur d'autre part sont prises en compte. L'objectif était de déterminer la meilleure structure et les valeurs optimales des volumes des réacteurs qui permettent de minimiser le coût total tout en respectant les contraintes réglementaires sur les rejets.Par ailleurs, une optimisation multicritère de la station optimale résultante a été réalisée. Elle a permis de déterminer l'ensemble de Pareto des solutions qui minimisent la consommation énergétique (d'aération et de pompage) et maximisent la qualité de l'effluent. La quatrième et dernière partie de ce travail s'intéresse à la modélisation, simulation et optimisation de la station de traitement de Verulam près de Durban en Afrique du Sud. Des mesures expérimentales ont été réalisées sur cette station et le modèle ASM1 a été utilisé pour décrire son fonctionnement. Une analyse d'estimabilité des paramètres a été d'abord réalisée pour déterminer les paramètres du modèle qui peuvent être estimés à partir des mesures expérimentales disponibles. Les paramètres estimables ont ensuite été identifiés à l'aide de gProms. Le modèle ainsi identifié a été validé et ensuite utilisé pour optimiser le fonctionnement énergétique de cette station / This work is a direct extension of the PhD thesis of Chachuat (2001) on dynamic optimization and optimal control of small size wastewater treatment plants. The objective is to go further by focusing on optimal design and operation of wastewater treatment plants of any size. Thus, in a first part, optimization of small size wastewater treatment plants was studied. Contrary to what has been done so far: (i) the aeration is no longer alternating, but continuous, (ii) the settler is not considered perfect, but its operation is modeled using a series of 10 sedimentation layers, (iii) the optimization approach developed is based on the method of sensitivities implemented wthin the dynamic simulation and optimization software gProms, used throughout this work. The influence of the settler model on the minimization of aeration energy was particularly investigated. In a second part , the large size treatment plants are considered . More specifically, the benchmark model developed by the European network COST was used to describe their operation. A "foreign object" was developed in order to make the simulation and optimization of these plants possible using gProms. The optimisation showed that the aeration energy consumption could be reduced by at least 30 % compared to the current operation of these plants . In a third part, the optimization of the design of the wastewater treatment plant was studied. A superstructure has been defined with several (five) reactors and a settler. All the possibilities of recycling and by-passes between the reactors on the one hand and between the reactors and the settler on the other are considered. The objective was to determine the best structure and the optimal values of the reacter volumes that minimize the net present value while respecting the regulatory constraints. On the other hand, a multi-objective optimization problems of the treatment plant was carried out. It allawed to determine the Pareto set of solutions that minimize the energy consumption (pumping and aeration) and maximize the effluent quality. The fourth and last part of this work focuses on modeling, simulation and optimization of the treatment plant of the city of Verulam in the area of Durban in South Africa. Experimental measurements were carried out on the plant and the ASM1 model was used to describe its operation. An estimability analysis was first performed in order to determine the model parameters that can be estimated from the available experimental measurements . The estimable parameters were then identified using gProms . The identified model was validated and then used to optimize the energy function of this plant

La recherche de moyens alternatifs pour la propulsion d'un aéronef est primordiale tant la dépendance au pétrole est forte. Le travail proposé dans cette thèse s'inscrit dans le besoin de soutenir les concepteurs de systèmes de propulsion innovants utilisant l'électricité. En partant du constat qu'il est primordial de s'appuyer sur l'analyse de l'aéronef dans sa globalité, nous proposons une approche basée sur les modèles, faisant appel aux modèles d’ingénierie système, aux modèles comportementaux basés sur la physique et à la simulation numérique, et collaborative, car la conception implique de nombreux métiers.L'objectif de cette approche est la création d'un produit virtuel qui est un modèle global multidisciplinaire exécutable du produit pour en faciliter la conception. Une méthodologie est alors construite pour se concentrer sur la relation entre le produit virtuel, ses modèles constitutifs et leur obtention. Le fil directeur de la méthodologie correspond à une recherche d'informations, au moyen de l'analyse des interactions et impacts multidisciplinaires qui apparaissent dans le système, puis l'application de cette information pour la construction d'un modèle d'intention qui permet la requête de modèles comportementaux auprès d'experts. C'est finalement le lien manquant entre la conception globale conduite par l'ingénierie système et la conception basée sur la physique du monde réel qui est implicitement traité dans ces travaux. Pour réaliser l'ensemble de la méthodologie, un nouveau rôle a été défini, le rôle d'architecte de simulation. Cette thèse présente la méthodologie de manière théorique, incluant ses rôles et concepts, puis cette dernière est démontrée sur un cas d'étude correspondant à l'hybridation d'un drone de type hélicoptère. / The research of alternative aircraft propulsion system is mandatory because oil dependence is too strong. The work proposed in this thesis is oriented to support electric based innovative propulsion system designers. Considering that it is important to consider entire aircraft analysis, we propose a model based, with systems engineering models, physics-based behavioral models and numerical simulation, and collaborative, because design require numerous business expertise. The objective of this approach is to build a virtual product, which means a global multidisciplinary executable model of the product under design in order to facilitate its design. A methodology is then developed, focused on the relation between the virtual product, its constitutive models and their acquisition. The methodology director wire corresponds to information research, with multidisciplinary interactions and impacts in the system, and then the application of those pieces of information to build a model of intention which allows requesting a behavioral model from experts. Finally, it is the missing link between global design driven with systems engineering and real physics based design which is implicitly at stake. To perform the methodology, a new role has been defined, the simulation architect. This thesis presents theoretically the methodology, including roles and concepts, and then this methodology is demonstrated on a helicopter based drone study-case.

La consommation énergétique dans le secteur bâtiment dépend de diverses facteurs parmi lesquels ses caractéristiques physique, ses équipements, l’environnement extérieur, etc… mais il ne faut pas oublier le comportement des habitants qui est déterminant pour la consommation énergétique globale. Or, la plupart des travaux et outils représentent les occupants par des profils d’occupation. Cette thèse s’intéresse à la représentation plus détaillée du comportement des occupants, en particulier les mécanismes cognitifs, réactifs et délibératifs. Le comportement dynamique des occupants est modélisé et co-simulé avec les aspects physiques et des éventuels systèmes de gestion énergétique. L’analyse de la consommation de différents équipements électroménagers met en évidence que le consommation énergétique est très dépendante des comportements des occupants. L’analyse des consommations et des actions des habitants permet d’élaborer un modèle du comportement des occupants impactant la consommation énergétique. Le modèle représente des mécanismes cognitifs, qui représente les causes qui motivent les actions, incluant des échange avec d’autres acteurs humains. Une approche à base d’agents logiciels a été développée. Outre les aspects techniques, une méthodologie de réglage des paramètres des modèles de comportement est proposée. Ces outils sont utilisés pour réaliser une co-simulation représentant la physique du bâtiment, le comportement réactif, c’est-à-dire sensible aux données physiques, et délibératif des habitants mais aussi un système de gestion énergétique qui peut ajuster directement la configuration du logement ou simplement conseiller ces occupants. L’impact de différents types de comportements, avec et sans gestionnaire énergétique est analysé. Ces travaux ouvrent de nouvelles perspectives dans la simulation bâtiment, dans la validation de gestionnaires énergétiques mais aussi dans la représentation des bâtiments dans les réseaux d’énergie dits intelligents, dans lesquels des signaux peuvent être envoyés aux utilisateurs finaux pour les inviter à moduler leur consommation. / Energy consumption in buildings is affected by various factors including its physical characteristics, the appliances inside, and the outdoor environment, etc. However, inhabitants’ behaviour that determines the global energy consumption must not be forgotten. In most of the previous works and simulation tools, human behaviour is modelled as occupancy profiles. In this thesis the focus is more on detailed behaviour representation, particularly the cognitive, reactive, and deliberative mechanisms. The inhabitants’ dynamic behaviour is modelled and co-simulated together with the physical aspects of a building and an energy management system. The analysis of different household appliances has revealed that energy consumption patterns are highly associated with inhabitants’ behaviours. Data analysis of inhabitants’ actions and appliances’ consumptions is used to derive a model of inhabitants’ behaviour that impacts the energy consumption. This model represents the cognitive mechanisms that provide causes that motivate the actions, including the communication with other inhabitants. An approach based on multi-agent systems is developed along with a methodology for parameter tuning in the proposed behaviour model. These tools are used to co-simulate, not only the physical characteristics of the building, the reactive behaviour that is sensitive to physical data, and deliberative behaviour of the inhabitants, but also the building energy management system. The energy management system allows the direct adjustment of the building parameters or simply giving advice to the inhabitants. The impact of different types of inhabitants’ behaviours, with and without the inclusion of an energy management system is analyzed. This work opens new perspectives not only in the building simulation and in the validation of energy management systems but also in the representation of buildings in the smart grid where signals can be sent to end users advising them to modulate their consumption.

Cette thèse propose une méthodologie qui intègre les méthodes formelles dans la spécification, la conception, la vérification et la validation des systèmes complexes concurrents et distribués avec une perspective à événements discrets. La méthodologie est basée sur le langage graphique HILLS (High Level Language for System Specification) que nous avons défini. HiLLS intègre des concepts de génie logiciel et de théorie des systèmes pour une spécification des systèmes. Précisément, HiLLS intègre des concepts et notations de DEVS (Discrete Event System Specification), UML (Unified Modeling Language) et Object-Z. Les objectifs de HILLS incluent la définition d’une syntaxe concrète graphique qui facilite la communicabilité des modèles et plusieurs domaines sémantiques pour la simulation, le prototypage, l’enaction et l’accessibilité à l’analyse formelle. L’Enaction se définit par le processus de création d’une instance du système qui s’exécute en temps réel (par opposition au temps virtuel utilisé en simulation). HiLLS permet la construction hiérarchique et modulaire des systèmes à événements discrets grâce à une description simple et rigoureuse des aspects statiques, dynamiques et fonctionnels des modèles. La sémantique pour simulation de HiLLS est définie en établissant un morphisme sémantique entre HiLLS et DEVS; de cette façon chaque modèle HiLLS peut être simulé en utilisant un simulateur DEVS. Cette approche permet aux utilisateurs DEVS d’utiliser HiLLS comme un langage de spécification dans la phase de modélisation et d’utiliser leurs propres implémentations locales ou distribuées de DEVS en phase de simulation. L’enactment des modèles HiLLS est basé sur une adaptation du patron de conception Observateur pour leur implémentation. La vérification formelle est faite en établissant un morphisme entre chaque niveau d’abstraction de HiLLS et une méthode formelle adaptée pour la vérification formelle des propriétés à ce niveau. Les modèles formels sur lesquels sont faites les vérifications formelles sont obtenus à partir des spécifications HiLLS en utilisant des morphismes. Les trois niveaux d’abstraction de HiLLS sont : le niveau composite, le niveau unitaire et le niveau des traces. Ces niveaux correspondent respectivement aux trois niveaux suivants de la hiérarchie de spécification des systèmes proposée par Zeigler : CN (Coupled Network), IOS (Input Output System) et IORO (Input Output Relation Observation). Nous avons établi des morphismes entre le niveau Composite et CSP (Communicating Sequential Processes), entre le niveau unitaire et Z, et nous utilisons les logiques temporelles telles que LTL, CTL et TCTL pour exprimer les propriétés sur les traces. HiLLS permet à la fois la spécification des modèles à structures statiques et les modèles à structures variables. Dans le cas des systèmes à structures variables, le niveau composite intègre à la fois des propriétés basées sur les états et les processus. Pour prendre en compte ces deux aspects, un morphisme est défini entre le niveau Composite de HiLLS et CSPZ (une combinaison de CSP et Z). Le processus de vérification et de validation combine la simulation, la vérification exhaustive de modèle (model checking) et la preuve de théorèmes (theorem proving) dans un Framework commun. La vérification exhaustive et la preuve de théorèmes sur les modèles HiLLS sont basées sur les outils associés aux méthodes formelles sélectionnées dans les morphismes. Nous appliquons la méthodologie de modélisation de HiLLS à la modélisation du Alternating Bit Protocol (ABP) et à celle d’un guichet automatique de dépôt de billet (Automated Teller Machine) (ATM). / This thesis proposes a methodology which integrates formal methods in the specification, design, verification and validation processes of complex, concurrent and distributed systems with discrete events perspectives. The methodology is based on the graphical language HILLS (High Level Language for System Specification) that we defined. HiLLS integrates software engineering and system theoretic views for the specification of systems. Precisely, HiLLS integrates concepts and notations from DEVS (Discrete Event System Specification), UML (Unified Modeling Language) and Object-Z. The objectives of HILLS include the definition of a highly communicable graphical concrete syntax and multiple semantic domains for simulation, prototyping, enactment and accessibility to formal analysis. Enactment refers to the process of creating an instance of system executing in real-clock time. HILLS allows hierarchical and modular construction of discrete event systems models while facilitating the modeling process due to the simple and rigorous description of the static, dynamic, structural and functional aspects of the models. Simulation semantics is defined for HiLLS by establishing a semantic mapping between HiLLS and DEVS; in this way each HiLLS model can be simulated by a DEVS simulator. This approach allow DEVS users to use HiLLS as a modeling language in the modeling phase and use their own stand alone or distributed DEVS implementation package to simulate the models. An enactment of HiLLS models is defined by adapting the observer design-pattern to their implementation. The formal verification of HiLLS models is made by establishing morphisms between each level of abstraction of HILLS and a formal method adapted for the formal verification of the properties at this level. The formal models on which are made the formal verification are obtained from HILLS specifications by using the mapping functions. The three levels of abstraction of HILLS are: the Composite level, the Unitary level and the Traces level. These levels correspond respectively to the following levels of the system specification hierarchy proposed by Zeigler: CN (Coupled Network), IOS (Input Output System) and IORO (Input Output Relation Observation). We have established morphisms between the Composite level and CSP (Communicating Sequential Processes), between Unitary level and Z and we expect to use temporal logics like LTL, CTL and TCTL to express traces level properties. HiLLS allows the specification of both static and dynamic structure systems. In case of dynamic structure systems, the composite level integrates both sate-based and process-based properties. To handle at the same time state-based and process-based properties, morphism is established between the dynamic composite level and CSPZ (a combination of CSP and Z); The verification and validation process combine simulation, model checking and theorem proving techniques in a common framework. The model checking and theorem proving of HILLS models are based on an integrated tooling framework composed of tools supporting the notations of the selected formal methods in the established morphisms. We apply our methodology to modeling of the Alternating Bit Protocol (ABP) and the Automated Teller Machine (ATM).

La recherche de moyens alternatifs pour la propulsion d'un aéronef est primordiale tant la dépendance au pétrole est forte. Le travail proposé dans cette thèse s'inscrit dans le besoin de soutenir les concepteurs de systèmes de propulsion innovants utilisant l'électricité. En partant du constat qu'il est primordial de s'appuyer sur l'analyse de l'aéronef dans sa globalité, nous proposons une approche basée sur les modèles, faisant appel aux modèles d’ingénierie système, aux modèles comportementaux basés sur la physique et à la simulation numérique, et collaborative, car la conception implique de nombreux métiers.L'objectif de cette approche est la création d'un produit virtuel qui est un modèle global multidisciplinaire exécutable du produit pour en faciliter la conception. Une méthodologie est alors construite pour se concentrer sur la relation entre le produit virtuel, ses modèles constitutifs et leur obtention. Le fil directeur de la méthodologie correspond à une recherche d'informations, au moyen de l'analyse des interactions et impacts multidisciplinaires qui apparaissent dans le système, puis l'application de cette information pour la construction d'un modèle d'intention qui permet la requête de modèles comportementaux auprès d'experts. C'est finalement le lien manquant entre la conception globale conduite par l'ingénierie système et la conception basée sur la physique du monde réel qui est implicitement traité dans ces travaux. Pour réaliser l'ensemble de la méthodologie, un nouveau rôle a été défini, le rôle d'architecte de simulation. Cette thèse présente la méthodologie de manière théorique, incluant ses rôles et concepts, puis cette dernière est démontrée sur un cas d'étude correspondant à l'hybridation d'un drone de type hélicoptère. / The research of alternative aircraft propulsion system is mandatory because oil dependence is too strong. The work proposed in this thesis is oriented to support electric based innovative propulsion system designers. Considering that it is important to consider entire aircraft analysis, we propose a model based, with systems engineering models, physics-based behavioral models and numerical simulation, and collaborative, because design require numerous business expertise. The objective of this approach is to build a virtual product, which means a global multidisciplinary executable model of the product under design in order to facilitate its design. A methodology is then developed, focused on the relation between the virtual product, its constitutive models and their acquisition. The methodology director wire corresponds to information research, with multidisciplinary interactions and impacts in the system, and then the application of those pieces of information to build a model of intention which allows requesting a behavioral model from experts. Finally, it is the missing link between global design driven with systems engineering and real physics based design which is implicitly at stake. To perform the methodology, a new role has been defined, the simulation architect. This thesis presents theoretically the methodology, including roles and concepts, and then this methodology is demonstrated on a helicopter based drone study-case.

Les outils de simulation sont des moyens pour faciliter la mise en place d'une production sur les Machines Outil à Commande Numérique, ces outils sont devenus très courants dans l'industrie et, par conséquent, dans l'éducation. Plusieurs problèmes importants émergent, telles que des questions d’ordre pédagogique, des aspects liés à l’ergonomie des interfaces, le coût d'acquisition de l'équipement et d'adaptabilité des étudiants aux multitudes de logiciels de fabrication assistée par ordinateur, de ce fait le problème de la sélection du logiciel est soulevé dans l'éducation afin d'assurer une efficacité des processus d'enseignement et d'apprentissage des étudiants.Cette thèse est conduite dans l’objectif d’étudier une méthodologie pour sélectionner un logiciel de FAO qui pourrait être efficace en tant que support d’apprentissage de la FAO en premier cycle des universités techniques, des écoles d’ingénieurs et autres établissements similaires. Les facteurs déterminants l’efficacité des étudiants utilisant un logiciel dans leurs apprentissages de la FAO ont été déduits du cadre théorique de la thèse qui s’est basé sur la théorie de l’activité. Cette théorie prend en considération le contexte global de cette activité d’enseignement-apprentissage de la FAO à savoir l’étudiant, l’artefact, le professeur, l’établissement et la communauté des éditeurs de logiciels.Le traitement statistique des données recueillies à travers les réponses d’un échantillon de 50 étudiants ont été élaboré dans le but de confirmer nos hypothèses sur les principaux critères d'évaluation de logiciel de simulation en éducation. / Simulation tools as means to facilitate setting up a production have become very common in industry and, therefore, in education. Among several significant problems, like pedagogical issues, the cost of equipment acquisition and the adaptability of students to the multitude of Computer-Aided Manufacturing, it is raise in education the problem of selecting software in order to ensure maximum effectiveness of teaching process and students learning.This research study was designed to investigate a methodology to select CAM software that could be effective as a support of CAM learning in university, taking into account different features of CAM learning. We determine the student effectiveness in learning factors of CAM software and further, determine the relationship between the different main factors. The research was conducted using a questionnaire submitted to 50 students attending the second academic year of Mechanical Design and Production. The study provides results from empirical test of these relationships and provides criteria for evaluation simulation of software in education.

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.

Ce travail s'inscrit dans le cadre de l'évaluation de la sûreté de fonctionnement des systèmes commandés en réseau (SCR). La capacité des systèmes de commandes à compenser les effets de certaines défaillances de composants amène à redéfinir le concept de défaillances du système. La conséquence est que l'évaluation de la fiabilité prévisionnelle du système est dépendante de l'évaluation fonctionnelle et devient impossible avec les méthodes traditionnelles de la sûreté de fonctionnement. Pour surmonter ces difficultés, une approche basée sur la modélisation en vue de la simulation est proposée. Nous avons choisi les Réseaux d'activités stochastiques (SAN) largement connus dans la modélisation des protocoles de communication ainsi que dans les études de la sûreté de fonctionnement. Dans un premier temps, nous avons cherché à identifier l'incidence de deux types de défaillances fugitives : la perte d'un échantillon d'une part et le retard d'un échantillon dans la boucle de régulation d'autre part. Après, nous simulons le comportement en présence des deux types de perturbations simultanément, mettant en évidence des effets cumulatifs. Si on tient compte maintenant du fait que l'origine des pertes ou retards est due à la présence du réseau, il faut l'introduire dans le modèle. On introduit alors dans le modèle global du système la représentation SAN d'un réseau CAN et l'injection des défaillances dans celui-ci. La méthode de Monte Carlo est utilisée pour estimer les indicateurs de sûreté de fonctionnement et on montre l'influence de certains facteurs comme la charge du réseau par exemple. Nous avons proposé une méthode et les outils associés pour approcher cette évaluation par simulation et ainsi apporter une aide à la conception des systèmes satisfaisant à des exigences critiques sur certains paramètres de performance.