Dissertations / Theses on the topic 'Validation des exigences'

Aujourd’hui, de nombreux grands industriels de différents domaines se sont lancés dans la conception de produits intelligents pour répondre aux nouveaux besoins du marché. La conception de ces systèmes est de plus en plus complexe, puisqu’ils sont composés de nombreux composants physiques pouvant être contrôlés par des applications s'exécutant sur des processeurs. Afin d'assister cette conception multi-disciplines, la solution que nous proposons dans cette thèse est de diriger la modélisation et la conception du système par la prise en compte des scénarios de test qui devront être utilisés pour valider ses exigences. La méthode préconisée suggère de raisonner au niveau système et de commencer le processus de conception par la formalisation des tests de validation. En d'autres termes, il s'agit en particulier de préciser le(s) critère(s) d’acceptation de l’exigence ainsi que le scénario de test nécessaire pour le(s) vérifier. Formaliser ainsi les tests permet notamment d'analyser la formulation des exigences elles-mêmes et d'y lever toute ambiguïté. Nous proposons un modèle générique de la vue structurelle de l'infrastructure de test, et un profil UML associé. La vue comportementale est modélisée sous forme de diagrammes de séquences SysML. Les interfaces de l'infrastructure de test fournissent des contraintes de testabilité pour le système à concevoir. Nous avons développé un outil, ARES (Automatic geneRation of Executable tests from SysML), qui transforme automatiquement cette spécification structurelle/comportementale des tests en scénarios simulables ou exécutables. Ceux-ci, analogues par construction, seront utilisés pour valider des modèles simulables du système (Matlab/Simulink) puis lors du processus de vérification finale du produit (avec un environnement TestStand). Nous présentons l'application de cet outil sur diverses études de cas associées à des produits Schneider Electric<br>Nowadays, many major manufacturers in different fields are working towards the design of smart products to meet new market needs. The design of these systems is increasingly complex, as they are composed of many physical components controlled by applications running on processors. In order to support this multi-disciplinary design, the solution we propose in this thesis is to guide the system modeling and design by taking into account the test scenarios that will be used to validate its requirements. The method that we propose suggests reasoning at the system level and starting the design process by formalizing validation tests. In other words, it amounts to specifying the acceptance criterion(s) for the requirement as well as the test scenario necessary to verify it. Formalizing the tests in this way makes it possible to analyze the formulation of the requirements themselves and to remove any ambiguity. We propose a generic model of the structural view of the test infrastructure, and an associated UML profile. The behavioral view is modeled as SysML sequence diagrams. The test infrastructure interfaces provide testability constraints for the system to be designed. We have developed a tool, ARES (Automatic GeneRation of Executable Tests from SysML), which automatically transforms this structural/behavioral specification of the tests into simulatable or executable scenarios. These scenarios, analogous by construction, will be used to validate simulatable models of the system (Matlab/Simulink), then during the process of final verification of the product (with a TestStand environment). We present the application of this tool on various case studies associated with Schneider Electric products

La sécurité est un enjeu majeur dans le cycle de développement des systèmes critiques, notamment dans le secteur du transport ferroviaire. Cette thèse vise la modélisation, la vérification et la validation des règles d'exploitation ferroviaires au regard des exigences de sécurité. Ces règles ont pour but de définir les autorisations de déplacement des trains sur des lignes ferroviaires nationales équipées du système européen de gestion du trafic ferroviaire (ERTMS). De manière analogue, on trouve les concepts liés aux autorisations dans la description des politiques de contrôle d'accès des systèmes d'information. Par conséquent, nos contributions portent sur l'adaptation d'une approche UML/B pour le contrôle d'accès des systèmes d'information afin de modéliser et de valider les règles d'exploitation ferroviaires. Dans un premier temps, nous avons adapté le modèle Role Based Access Control (RBAC) sur une étude de cas ferroviaire extraite des règles d'exploitation appliquées sur la ligne à grande vitesse LGV Est-Européenne en France. La plate-forme B4MSecure nous a permis de modéliser ces règles à l'aide d'un profil UML de RBAC inspiré de SecureUML. Ensuite, ces modèles sont transformés en des spécifications B qui ont été enrichies par des propriétés de sécurité ferroviaire et soumises à des activités de vérification et de validation formelles. Aux concepts du modèle RBAC, le modèle Organization Based Access Control (Or-Bac) introduit la notion d'organisation, au centre de ce modèle, et la notion de contexte. Nous avons donc proposé d’utiliser ce modèle en tant qu’extension du modèle RBAC dans l’optique d’une interopérabilité ferroviaire en ERTMS<br>The safety is a major issue in the development cycle of the critical systems, in particular in the rail transportation sector. This thesis aims at the modeling, the verification and at the validation of the railway operating rules with regard to the safety requirements. These rules intend to define the authorizations of trains movement on national railway lines equipped with the European Rail Traffic Management System (ERTMS). In a similar way, we find the concepts of authorizations in the description of access control policies of information systems. Consequently, our contributions concern the adaptation of an UML/B approach for the access control of information systems to model and validate the railway operating rules. At first, we adapted the Role Based Access Control (RBAC) model on a railway case study extracted from the operating rules applied on the LGV-Est-Européenne line in France. The B4MSecure platform enables the modeling of these rules by means of a UML profile of RBAC inspired by SecureUML. Then, these models are transformed into B specifications. which are enhanced by railway safety properties and formally verified and validated. In addition to the concepts of the RBAC model, the Organization Based Access Control (Or-Bac) model introduces the notion of organization, in the center of this model, and the notion of context. We have therefore proposed to use this model as extension of the RBAC model in the context of railway interoperability in ERTMS

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit<br>The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

Le développement de spécifications formelles correctes pour des systèmes et logiciels commence par l’analyse et la compréhension des besoins du client. Entre ces besoins décrits en langage naturel et leur spécification définie dans un langage formel précis, un écart existe et rend la tâche de développement de plus en plus difficile à accomplir. Nous sommes face à deux mondes distincts. Ce travail de thèse a pour objectif d’expliciter et d’établir des interactions entre ces deux mondes et de les faire évoluer en même temps. Par interaction, nous désignons les liens, les échanges et les activités se déroulant entre les différents documents. Parmi ces activités, nous présentons la validation comme un processus rigoureux qui démarre dès l’analyse des besoins et continue tout au long de l’élaboration de leur spécification formelle. Au fur et à mesure du développement, des choix sont effectués et les retours des outils de vérification et de validation permettent de détecter des lacunes aussi bien dans les besoins que dans la spécification. L’évolution des deux mondes est décrite via l’introduction d’un nouveau besoin dans un système existant et à travers l’application de patrons de développement. Ces patrons gèrent à la fois les besoins et la spécification formelle associée ; ils sont élaborés à partir de la description de la forme des besoins. Ils facilitent la tâche de développement et aident à éviter les risques d’oublis. Quel que soit le choix, des questions se posent tout au long du développement et permettent de déceler des lacunes, oublis ou ambiguïtés dans l’existant<br>The development of correct formal specifications for systems and software begins with the analysis and understanding of client requirements. Between these requirements described in natural language and their specification defined in a specific formal language, a gap exists and makes the task of development more and more difficult to accomplish. We are facing two different worlds. This thesis aims to clarify and establish interactions between these two worlds and to evolve them together. By interaction, we mean all the links, exchanges and activities taking place between the different documents. Among these activities, we present the validation as a rigorous process that starts from the requirements analysis and continues throughout the development of their formal specification. As development progresses, choices are made and feedbacks from verification and validation tools can detect shortcomings in requirements as well as in the specification. The evolution of the two worlds is described via the introduction of a new requirement into an existing system and through the application of development patterns. These patterns manage both the requirements and their associated formal specifications ; they are elaborated from the description of the form of the requirements in the client document. They facilitate the task of development and help to avoid the risk of oversights. Whatever the choice, the proposed approach is guided by questions accompanying the evolution of the whole system and makes it possible to detect imperfections, omissions or ambiguities in the existing

Le corps de ce travail concerne la modélisation des systèmes à événements discrets. Il s'intéresse par ailleurs en quasi exclusivité à la gestion des contraintes de temps de séjour. Mes travaux de thèse ont comporté la constitution du cahier des charges en amont et les applications en aval d'un outil de modélisation des exigences temporelles : Les Réseaux de Petri P-temporels. L'ensemble de mes travaux de recherche a été développé dans le but d'asseoir l'utilisation de cet outil. Un premier axe a été de positionner l'outil par rapport à ceux de l'état de l'art. Une deuxième tâche a été de prouver un certains nombre de propriétés mathématiques dans l'optique de permettre des applications industrielles efficaces. Au delà de la stricte recherche de propriété, l'extension du champ applicatif, vers le domaine du ferroviaire par exemple, a pris une part très importante. Une troisième activité a débouché sur la caractérisation des limites du modèle et la proposition d'extension fonctionnelle ou de rapprochement de l'outil de modélisation vers des modèles existants. Ce modèle concerne donc les Systèmes à Evénements Discrets où l'on rencontre des contraintes de temps de séjour maximum dans un état donné. C'est le cas de la galvanoplastie qui a été le premier support applicatif. Très rapidement, le champ des applications potentielles de l'outil a été élargi par des publications dans les domaines de l'industrie alimentaire. Les travaux se sont par ailleurs concentrés sur la partie commande, en supposant que la séquence des opérations avait déjà été fixée. Ils ont été appuyés par le travail de master de recherche de M.F. Karoui en 2004 (deux conférences ont été publiées dans la suite de son mémoire). Par ailleurs, l'expertise en supervision qui se trouvait au sein de l'équipe Système à Evénement Discret a été valorisée par le stage de master de T. Lecuru sur la supervision des ateliers automobiles en 2003. Ce travail a pris une autre ampleur avec la thèse de Jerbi Nabil sur la commande des ateliers à contraintes de temps soutenue en 2006 (3 publications de revue). Il se poursuit avec la thèse de Annis Mhalla. En 2006, F. Defossez soutient un master dans le domaine ferroviaire sur la gestion des exigences temporelles de sécurité. Ce dernier va s'inscrire en troisième année de thèse et a déjà publié 5 conférences. Ce travail ouvre un champ très important pour l'outil de modélisation que je porte. Par exmple, cela a amné la participation à un projet Européen. Ce projet SELCAT qui s'intéresse au passage à niveau et qui s'est terminé en juin 2008. Il se prolongera dans un projet national ANR accepté qui débutera autour de janvier 2009. En parallèle, un projet spécifique ayant trait aux outils de modélisation sur les chantiers est en cours avec la SNCF. Enfin, la thèse de Hedi Dhouibi a été l'occasion de proposer un nouveau modèle capable de généraliser certaines propriétés des Réseaux de Pétri P-temporels à des systèmes où le paramètre critique est différent du temps. Une validation industrielle sur des données réelles a pu être effectuée (soutenance en 2005). Elle fait l'objet de trois publications de revues internationales (acceptation en 2008).

La contribution de cette thèse est une approche de génération automatique de tests fonctionnels à partir des exigences, prenant en compte la maîtrise du coût de test, l'adaptabilité au contexte des lignes de produits, la compatibilité avec les pratiques industrielles et la complexité des logiciels réels. Notre approche se base sur un modèle de cas d'utilisation étendus, relié à un analyseur de langage naturel contrôlé en amont et un générateur de tests en aval. Le langage contrôlé rapproche la méthode des pratiques industrielles, et formalise assez les exigences pour les transformer en un modèle de cas d'utilisation simulables (via l'ajout de contrats interprétables). Des critères de test permettent alors de générer des objectifs de test de haut niveau, qui sont ensuite raffinés vers des cas de test en utilisant des scénarios. La variabilité dans les exigences est prise en compte à chaque niveau de la génération de tests, cette approche est donc adaptée aux lignes de produits.

Les phases de validation et de vérification (V&amp;V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&amp;V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&amp;V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS<br>Reactive real time systems are critical systems. These systems requirements validation and verification (V&amp;V) activities are very important in terms of cost and time. Therefore, methods and tools that can alleviate and efficiently support V&amp;V activities are of great interest for aeronautic domain. Functional testing is the most commonly used technique for these systems requirements V&amp;V. But, testing methods present some limits: exhaustive test data generation is practically impossible because of the size and the complexity of these systems. In this way, controlling testing effort (complexity and cost) is major, but systems quality demands are very huge. Testing effort characterizes as well the tests definition as the diagnosis. In this perspective, we defined two methodologies based on testability analysis concepts and test strategies. The first methodology aims at guiding relevant functional tests definition and facilitating AIRBUS reactive systems SCADE data flow specification coverage analysis during the validation activities. The second methodology proposes methods supporting the verification activities (relevant tests definition for diagnosis and faulty component identification) based on functional testing on AIRBUS Final Assembly Line (FAL)

Les phases de validation et de vérification (V&V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS.

Les travaux développés dans cette thèse visent à assister le processus d’ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l’utilisateur durant l’expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l’ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d’incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L’idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d’observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d’observation (ou observateurs) ; chacun des patterns développés est relatif à un type d’exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d’accessibilité des états correspondants à la violation de l’exigence associée<br>The work developed in this thesis aims to assist the engineering process of temporal requirements for time-constrained complex systems. Our contributions concern three phases: the specification, the behaviour modelling and the verification. For the specification of temporal requirements, a new temporal properties typology taking into account all the common requirements one may meet when dealing with requirements specification, is introduced. Then, to facilitate the expression, we have proposed a structured English grammar. Nevertheless, even if each requirement taken individually is correct, we have no guarantee that a set of temporal properties one may express is consistent. Here we have proposed an algorithm based on graph theory techniques to check the consistency of temporal requirements sets. For the behaviour modelling, we have proposed an algorithm for transforming UML State Machine with time annotations into Timed Automata (TA). The idea is to allow the user manipulating a quite intuitive notation (UML SM diagramsduring the modelling phase and thereby, automatically generate formal models (TA) that could be used directly by the verification process. Finally, for the verification phase, we have adopted an observer-based technique. Actually, we have developed a repository of observation patterns where each pattern is relative to a particular temporal requirement class in our classification. Thereby, the verification process is reduced to a reachability analysis of the observers’ KO states relatives to the requirements’ violation

Les travaux développés dans cette thèse visent à assister le processus d'ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l'utilisateur durant l'expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l'ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d'incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L'idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d'observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d'observation (ou observateurs) ; chacun des patterns développés est relatif à un type d'exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d'accessibilité des états correspondants à la violation de l'exigence associée

Les travaux développés dans ce mémoire concernent la formalisation d'un processus sûr d'automatisation en vue de maîtriser la complexité induite par l'intégration de plus en plus importante de technologies de l'information et de la communication au cœur même des processus de production et des produits. Plus précisément, notre travail porte sur l'intégration d'approches méthodologiques, issues du Génie Automatique, et de modèles formels, issus du Génie Informatique et de l'Automatique des Systèmes à Evénements Discrets afin de garantir, a priori, le respect des exigences formulées par les utilisateurs. Notre contribution porte sur deux axes. Le premier concerne l'intégration de techniques de synthèse de la commande dans un processus d'automatisation, incluant les phases de modélisation et de génération d'un code implantable, et leur application à la reconfiguration de systèmes manufacturiers contrôlés par le produit. Le second est basé sur le raffinement formel ou semi-formel de modèles pour identifier et structurer les exigences exprimées à un niveau " système " puis les allouer et les projeter sur une architecture de fonctions, de composants ou d'équipements. Ces travaux ont été initiés dans le cadre de notre thèse en réponse aux besoins de R&D industriels de la Direction des Etudes & Recherche d'EDF, puis ont été poursuivis avec une cible relative aux systèmes manufacturiers et validés dans le cadre de collaborations industrielles variées.

Une entreprise, et particulièrement une PME ou une PMI, doit être apte à évoluer sur des secteurs d’activités souvent très concurrentiels qui évoluent rapidement, par exemple, en fonction d’une clientèle volatile et soucieuse de trouver des produits et des services moins chers et plus adaptés à ses besoins. La PME se trouve alors confrontée à des problèmes de réactivité et de flexibilité face à cette clientèle. Par effet direct, elle recherche à réduire les délais et les coûts de réalisation tout en privilégiant aussi la qualité et le degré d’innovation des biens et des services qu’elle propose. Le système d’information de cette PME est un enjeu essentiel pour mettre en œuvre cette stratégie et maximiser donc la réactivité et la flexibilité mais aussi la rentabilité et la qualité recherchées. Ce sont des qualités incontournables, garantes d’une autonomie et d’une reconnaissance dont la PME a grand besoin. Le système d’information est en effet la courroie de transmission entre le système de décision et le système productif qui génère la valeur ajoutée de la PME. Il fait le lien entre les différents acteurs de l’organisation mais aussi avec les partenaires externes de l’entreprise. Une partie de ce système d’information est de fait informatisée. Celui-ci supporte, mémorise et traite les informations nécessaires aux différents processus de décision, métier et support qui tapissent l’organisation pour servir la stratégie de l’entreprise. Les fonctionnalités, les interfaces et les données qui forment ce système informatisé sont donc cruciales à comprendre, à développer en accord avec les besoins de la PME, à améliorer au fur et à mesure de l’évolution de ces besoins. La PME est donc tentée de se lancer, seule ou accompagnée, dans des projets dits d’informatisation i.e. des projets visant le développement ou l’amélioration de son système informatisé. Nous nous intéressons ici à des projets visant à développer des applicatifs de gestion et de pilotage de la PME. La PME – prenant alors le rôle de la maîtrise d’ouvrage (MOA) – tout comme la société de services qui l’accompagne – prenant alors en charge le rôle de maîtrise d’œuvre (MOE) – doivent partager une vision commune des besoins d’informatisation. Elles sont alors appelées à mener en commun des activités d’ingénierie des besoins et des exigences (IBE). L’IBE guide et accompagne la PME pour arriver à décrire et formaliser ses besoins. Elle permet ensuite à la société de service de spécifier de manière plus formelle ces besoins sous forme d’exigences qui définissent alors les travaux de développement souhaités. L’IBE est souvent réalisée avec une assistance à maitrise d’ouvrage. Cette étape cruciale reste cependant difficile pour une PME. Elle est de plus souvent réalisée par la MOE elle-même pour faire face au manque de moyens, de temps et de compétences de la PME. Or, l’implication des collaborateurs de la PME est primordiale pour la réussite de tout projet d’informatisation, surtout si celui-ci impacte durablement le fonctionnement de la PME.Ces travaux, développés dans le cadre d’une collaboration Industrie/recherche avec la SSII RESULIS, ont consisté à développer une méthode d’IBE qui offre aux PME des concepts, des langages et des moyens de modélisation et de vérification simples mais suffisants tout en tant aisément manipulables de manière intuitive et donnant lieu à une formalisation pertinente pour la MOE. Cette méthode est basée sur le croisement et la complémentarité de principes issus de la Modélisation d’Entreprise et de l’Ingénierie Système pour l’élicitation de besoins. Des moyens de vérification et de validation semi-formels sont appliqués pour garantir certaines qualités attendues des exigences résultantes. La méthode s’intègre également au cycle de développement basé sur les modèles pour permettre a posteriori d’accélérer la production de prototypes et de rendre interopérables les langages et outils de la MOA et de la MOE<br>Most enterprises, and especially SMEs, must develop their business in very competitive and rapidly changing fields. Where they have to adapt to volatile customers who want to find cheaper products and services and that are more corresponding to their needs. The SME is then confronted with problems of responsiveness and flexibility in responding to these customers. As an effect, it seeks to reduce the costs and time to market and to provide high quality and innovative goods and services. The SME’s information system is an asset on which it can rely to implement this strategy and so to maximize its responsiveness and flexibility but also to reach the sought profitability and quality. These are key qualities that guarantee autonomy and recognition, qualities that are highly needed by any SME. The Information system is indeed the drive belt of information not only inside the enterprise, between decision and operational systems proving added value of the enterprise, but also within its environment that includes its external partners. Part of this information system is computerized. It stores and processes the information needed by the different decision-making, business and support processes that serve the enterprise’s strategy. It is crucial to understand the features, interfaces and data that make up this computerized system and develop them according to the needs of SME. The SME is therefore tempted to embark, alone or accompanied, in so-called computerization projects i.e. projects for the development or improvement of its computerized system. We are interested in projects aimed at developing management applications of SMEs. The SME – then assuming the role of project owner – along with the development team – supporting the role of project management – have to share a common vision of the computerization needs. They are then called upon to carry out jointly requirements engineering (RE) activities. RE guides the SMEs to be able to describe and formalize its needs. It then allows the development team to specify more formally these needs as requirements which then define the required development work. RE is often carried out with the assistance of project owner support. This crucial step remains difficult for SMEs. It is most often performed by the development team itself to address the lack of resources, time and skills of SMEs. However, the involvement of the SME’s members is vital to the success of any computerization project, especially if it permanently affects the functioning of the enterprise.This work, developed through a collaborative with the company RESULIS, consisted in developing a requirements engineering method which offers SMEs concepts, simple languages, modeling and verification means that are easily and intuitively manipulated and provide sufficient and relevant formalization of the SME’s requirements. This method is based on principles derived from both enterprise modeling and systems engineering fields for requirements elicitation. Semi-formal verification and validation means are applied to guarantee some expected qualities of the resulting requirements. The method is also integrated in the model driven development cycle to enable a posteriori the production of prototypes and make interoperable the languages and tools used by both the SME and the development team

Dans le cadre de nos activités de recherche, nous nous sommes intéressés à la mise en sécurité des systèmes dits critiques (pouvant en cas de défaillance causer des dommages sérieux aux personnes ou aux biens). La mise en sécurité de tels systèmes passe par l'expression de recommandations liées à la sécurité. Ces recommandations peuvent provenir d'une demande du client (clauses du cahier des charges), de l'état de l'art, d'un référentiel légal (normes, décrets, arrêtés,. . ) ou d'études sur les conséquences des défaillances du système sur l'environnement, les personnes, l'image de marque de l'entreprise, etc. À partir des recommandations introduites dans le cahier des charges du client, il est donc possible d'identifier des "exigences". Il faudra alors démontrer que ces exigences sont prises en compte sur l'ensemble du cycle de réalisation du système. Dans le cadre de cette thèse, nous proposons une méthode et des exemples de mise en œuvre qui se basent sur l'identification, l'expression et la vérification des exigences liées à la sécurité<br>Within the framework of our research activities, we were interested in the safety of critical systems (whose failure can cause serious damage to people, goods or environment). The design of the safety of such systems requires the expression of safety-related recommendations. These recommendations can come from requirements of the customer (contractual clauses), from the state of the art, from legal reference frame (standards, decrees, laws) or from studies of the consequences of the failures on the system, the people, the environment. Starting from the safety recommendations coming from contractual conditions of the customer, it is thus possible to identify "safety requirements". It will have then to be proved that these safety requirements are taken into account during the whole design and lifecycle of the system. Within the framework of this thesis, we propose a method and implementation examples, which are based on the identification, the expression and the verification of the safety requirements

L’ingénierie système est un domaine où l’on étudie la conception de systèmes complexes. Un système est une solution que l’on veut développer, par exemple un train ou un réseau de satellites. Un système complexe est composé de différents éléments indépendants. Les ingénieurs travaillent à partir de listes d’attentes vis à vis du système, chacune caractérisant ce qu’il doit être ou doit faire. Ils créent alors un système et vérifient qu’il répond aux attentes. Afin de gagner du temps et de l’argent, on souhaite vérifier que le système correspond aux attentes avant même de le réaliser. Cela demande d’intégrer les différentes attentes et spécifier comment elles doivent être mises ensembles, générant ainsi un système attendu que l’on peut valider. Le but de la thèse est de fournir une méthode permettant d'intégrer les informations caractérisant un système de train au cours de sa conception, permettant ainsi la spécification, la représentation et la validation de son comportement<br>System engineering is a domain that studies the conception of complex system. A system corresponds to a solution we want to develop, such as a train, a satellite network, etc. A complex system is composed of several independent elements Engineers work from lists of individual expectations regarding the system to be or what it is supposed to do, which they use to create a system and see if it answers expectations. To gain time and money, we would like to check that the system-to-be answers expectations before developing it: it requires to integrate expectations and specify how they should be put together, inducing a system expected that we can check. The goal pursued in this PhD is to provide a method to integrate information regarding a train system during conception, enabling the specification, representation and validation of its behavior

Cette thèse a testé un modèle explicatif de santé psychologique au travail, intégrant comme variable bipolaire, l'épuisement professionnel et le bien-être psychologique. Sur la base du Job Demands-Resources Model, des facteurs d'exigences (conflits de rôles et charge de travail) et de ressources organisationnelles (justice organisationnelle, autonomie au travail et soutien social) ont été catégorisés. Le postulat de base de ce modèle a été de prédire des effets directs et indirects des exigences et des ressources sur la santé psychologique par l'intermédiaire de l'assertivité. L'objectif était la validation prévisionnelle et transculturelle du modèle, à travers une modélisation par équations structurelles, auprès de deux échantillons comprenant des enseignants et des infirmiers français et gabonais. L'effectif total de la première vague de données regroupait 273 participants (France : N = 90 enseignants, N = 45 infirmiers ; Gabon : N = 93 enseignants, N = 45 infirmiers) et celui de la deuxième vague s'élevait à 400 participants (France : N = 108 enseignants, N = 96 infirmiers ; Gabon : N = 141 enseignants, N = 55 infirmiers). En France, les résultats démontrent que les exigences au travail agissent directement sur la santé psychologique et que leurs effets sont aussi médiatisés par l'assertivité. Les ressources, pour leur part, influencent directement la santé psychologique. Quant aux résultats du Gabon, les exigences et les ressources organisationnelles prédisent directement la santé psychologique, sans effet médiateur de l'assertivité. De plus, au sein des deux populations, l'assertivité s'est avérée être non seulement une variable salutaire au regard des conditions de travail, mais aussi un fort prédicteur de la santé psychologique au travail<br>This thesis tested an explicative model of psychological well-being at work, including as a bipolar variable, burnout and psychological well-being. Based on the Job Demands-Resources Model, jobs demands (role conflict and workload) and job resources (organizational justice and social support) were categorized. The basic assumption of this model was to predict the direct and indirect effects of job demands-resources on psychological health at work through assertiveness. The goal was the previsional and transcultural validation of the model through structural equation modeling, with two samples : teachers and nurses French and Gabonese. The total of the first wave of data consisted of 273 participants (France : N = 90 teachers, N = 45 nurses ; Gabon : N = 93 teachers, N = 45 nurses) and the second wave was 400 partcicipants (France : N = 108 teachers, N = 96 nurses ; Gabon : N = 141 teachers, N = 45 nurses). In France, results demonstrate that the job demands act directly on the psychological health and their effects are also mediated by assertiveness. resources, in turn, directly affect psychological health. As for results of Gabon, job demands-resources directly predict psychological health, unmediated effect of assertiveness. In addition, in both populations, assertiveness is not only a beneficial variable compared to working conditions, but also a strong predictor of psychological health at work

Dans un avion, un hélicoptère ou un lanceur actuel, des milliers de capteurs, pour la plupart non critiques sont utilisés pour la mesure de divers paramètres (températures, pressions, positions...) Les résultats sont ensuite acheminés par des fils vers les calculateurs de bord qui les traitent. Ceci implique la mise en place de centaines de kilomètres de câbles (500 km pour un avion de ligne) dont le volume est considérable. Il en résulte une grande complexité de conception et de fabrication, des problèmes de fiabilité, notamment au niveau des connexions, et une masse importante. Par ailleurs l'instrumentation de certaines zones est impossible car leur câblage est difficilement envisageable par manque d'espace. En outre, s'il est souvent intéressant d'installer de nouveaux capteurs pour faire évoluer un aéronef ancien, l'installation des câbles nécessaires implique un démantèlement partiel, problématique et coûteux, de l'appareil. Pour résoudre ces problèmes, une idée innovante a émergé chez les industriels de l'aéronautique : commencer à remplacer les réseaux filaires reliant les capteurs d'un aéronef et leur centre de décision par des réseaux sans fil. Les technologies de communication sans fil sont aujourd'hui largement utilisées dans les marchés de l'électronique de grande consommation. Elles commencent également à être déployées pour des applications industrielles comme l'automobile ou le relevé à distance de compteurs domestiques. Cependant, remplacer des câbles par des ondes représente un défi technologique considérable comme la propagation en milieu confiné, la sécurité, la sureté de fonctionnement, la fiabilité ou la compatibilité électromagnétique. Cette thèse est motivée d'une part par l'avancée non négligeable dans le milieu aérospatial que pourrait être l'établissement d'un réseau sans fil à bord d'aéronefs dans la résolution de problématique classiques comme l'allégement et l'instrumentation. Il en résulterait donc : * Une meilleure connaissance de l'environnement et de la santé de l'aéronef * Un gain sur le poids. * Un gain en flexibilité. * Un gain en malléabilité et en évolutivité. * Un gain sur la complexité. * Un gain sur la fiabilité D'autre part, étant donnée la complexité de la conception de ce réseau de capteur sans fil, il a été nécessaire d'appliquer une méthodologie évolutive et adaptée mais inspirée de l'ingénierie système. Il est envisageable, vu le nombre de sous-systèmes à considérer, que cette méthodologie soit réutilisable pour d'autre cas pratiques. Une étude aussi complète que possible a été réalisée autour de l'existant déjà établi sur le sujet. En effet, on peut en lisant ce mémoire de thèse avoir une idée assez précise de ce qui a été fait. Une liste a été dressée de toutes les technologies sans fil en indiquant leur état de maturité, leurs avantages et leurs inconvénients afin de préciser les choix possibles et les raisons de ces choix. Des projets de capteurs sans fil ont été réalisés, des technologies sans fil performantes et personnalisables ont été développées et arrivent à maturité dans des secteurs variés tels que la domotique, la santé, l'automobile ou même l'aéronautique. Cependant aucun capteur sans fil n'a été véritablement installé en milieu aérospatial car de nombreux verrous technologiques n'ont pas été levés. Fort des expériences passées, et de la maturité qu'ont prise certaines technologies, des conclusions ont été tirées des projets antérieurs afin de tendre vers des solutions plus viables. Une fois identifiés, les verrous technologiques ont été isolés. Une personnalisation de notre solution a été à envisager afin de remédier tant que faire se peut à ces points bloquants avec les moyens mis à disposition. La méthodologie appliquée nous a permis d'identifier un maximum de contraintes, besoins et exigences pour mieux focaliser les efforts d'innovation sur les plus importantes et choisir ainsi les technologies les plus indiquées.