La modélisation informatique et la simulation sont des activités de plus en plus répandues lors de la conception de systèmes complexes et critiques tels que ceux embarqués dans les avions. Une proposition pour la conception et réalisation d'abstractions compatibles avec les objectifs de simulation est présentée basés sur la théorie de l'informatique, le contrôle et le système des concepts d'ingénierie. Il adresse deux problèmes fondamentaux de fidélité dans la simulation, c'est-à-dire, pour une spécification du système et quelques propriétés d'intérêt, comment extraire des abstractions pour définir une architecture de produit de simulation et jusqu'où quel point le comportement du modèle de simulation représente la spécification du système. Une notion générale de cette fidélité de la simulation, tant architecturale et comportementale, est expliquée dans les notions du cadre expérimental et discuté dans le contexte des abstractions de modélisation et des relations d'inclusion. Une approche semi-formelle basée sur l'ontologie pour construire et définir l'architecture de produit de simulation est proposée et démontrée sur une étude d'échelle industrielle. Une approche formelle basée sur le jeu théorique et méthode formelle est proposée pour différentes classes de modèles des systèmes et des simulations avec un développement d'outils de prototype et cas des études. Les problèmes dans la recherche et implémentation de ce cadre de fidélité sont discutées particulièrement dans un contexte industriel. / In using Modeling and Simulation for the system Verification & Validation activities, often the difficulty is finding and implementing consistent abstractions to model the system being simulated with respect to the simulation requirements. A proposition for the unified design and implementation of modeling abstractions consistent with the simulation objectives based on the computer science, control and system engineering concepts is presented. It addresses two fundamental problems of fidelity in simulation, namely, for a given system specification and some properties of interest, how to extract modeling abstractions to define a simulation product architecture and how far does the behaviour of the simulation model represents the system specification. A general notion of this simulation fidelity, both architectural and behavioural, in system verification and validation is explained in the established notions of the experimental frame and discussed in the context of modeling abstractions and inclusion relations. A semi-formal ontology based domain model approach to build and define the simulation product architecture is proposed with a real industrial scale study. A formal approach based on game theoretic quantitative system refinement notions is proposed for different class of system and simulation models with a prototype tool development and case studies. Challenges in research and implementation of this formal and semi-formal fidelity framework especially in an industrial context are discussed.

Devant l’augmentation de la part des énergies renouvelables en France, cette thèse propose d’étudier l’augmentation de la flexibilité des réacteurs à eau pressurisée en croisant deux disciplines pour, chacune, atteindre des objectifs complémentaires : l’Ingénierie Système (IS) et l’Automatique.Dans le contexte de l’ingénierie de systèmes complexes et du Model Based Systems Engineering, ce travail propose dans un premier temps une méthode de conception se fondant sur les principes normatifs de l’IS et respectant les habitudes et les pratiques courantes en ingénierie de Framatome. Cette méthode a pour vocation de formaliser et assurer le passage des exigences aux architectures et d’améliorer les capacités de vérification des modèles développés lors de la conception. Elle s’organise autour de langages de modélisation interopérables, couvrant l’ensemble des processus promus par l’IS. La méthode proposée est appliquée sur le système dont les performances sont les plus limitantes dans le contexte de l’augmentation de flexibilité : le Core Control. Ce composant algorithmique du réacteur assure le contrôle des paramètres de fonctionnement du cœur : la température moyenne, la distribution axiale de puissance et la position des groupes de grappes.La thèse propose ensuite des contributions techniques relevant du champ de l’Automatique. Il s’agit de concevoir un système de régulation répondant aux exigences issues de la formalisation IS évoquée ci-dessus. La solution proposée repose sur une stratégie de commande hiérarchisée, utilisant la complémentarité des approches dites de commande multi-objectif, de séquencement de gains et enfin de commande prédictive. Un modèle de réacteur nucléaire simplifié innovant est développé à des fins de conception du système de régulation et de simulations intermédiaires. Les résultats obtenus ont montré les capacités d’adaptation de la démarche proposée à des spécifications diverses. Les performances atteintes sont très encourageantes lorsque évaluées en simulation à partir d’un modèle réaliste et comparées à celles obtenues par les modes de pilotages classiques. / In the event of increasing renewable energies in France, this thesis proposes to study the flexibility increase of pressurized water reactors (PWR) throughout two different engineering disciplines aiming at complementary objectives: Systems Engineering (SE) and Control theory.In a first phase, within the frame of complex systems design and Model Based Systems Engineering, this work proposes a SE method based on SE standard principles and compliant with Framatome’s practices and addressing the revealed issues. This SE contribution is twofold: formalize and ensure the path from requirements to system architectures and enhance the capabilities of models verification. The method revolves around interoperable modeling languages, covering the SE processes: from requirement engineering to system architecture design. The method is applied to the system, which performances are the most limiting in the context of flexibility increase: the Core Control. This algorithmic reactor component ensures the control of: the average coolant temperature, the axial offset and the rod bank position, three of the core main functioning parameters.In order to provide a technical contribution relying on some advanced control methodologies. It consists in designing a control system meeting the requirements defined by the SE method application. The proposed solution is in a two-layer control strategy using the synergies of multi-objective control, gain-scheduling and predictive control strategies. A simplified innovative nuclear reactor model is employed to conceive the control algorithm, simulate and verify the developed models. The results obtained from this original approach showed the ability to adapt to various specifications. Compared to conventional core control modes, the simulation results showed very promising performances, while meeting the requirements, when evaluated on a realistic reactor model.

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 / 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 langages dédiés de modélisation (DSMLs) sont de plus en plus utilisés dans les phases amont du développement des systèmes complexes, en particulier pour les systèmes critiques embarqués. L’objectif est de pouvoir raisonner très tôt dans le développement sur ces modèles et, notamment, de conduire des activités de vérification et validation (V and V). Une technique très utilisée est la vérification des modèles comportementaux par exploration exhaustive (model-checking) en utilisant une sémantique de traduction pour construire un modèle formel à partir des modèles métiers pour réutiliser les outils performants disponibles pour les modèles formels. Définir cette sémantique de traduction, exprimer les propriétés formelles à vérifier et analyser les résultats nécessite une expertise dans les méthodes formelles qui freine leur adoption et peut rebuter les concepteurs. Il est donc nécessaire de construire pour chaque DSML, une chaîne d’outils qui masque les aspects formels aux utilisateurs. L’objectif de cette thèse est de faciliter le développement de telles chaînes de vérification. Notre contribution inclut 1) l’expression des propriétés comportementales au niveau métier en s’appuyant sur TOCL (Temporal Object Constraint Language), une extension temporelle du langage OCL; 2) la transformation automatique de ces propriétés en propriétés formelles en réutilisant les éléments clés de la sémantique de traduction; 3) la remontée des résultats de vérification grâce à une transformation d’ordre supérieur et un langage de description de correspondance entre le domaine métier et le domaine formel et 4) le processus associé de mise en oeuvre. Notre approche a été validée par l’expérimentation sur un sous-ensemble du langage de modélisation de processus de développement SPEM, et sur le langage de commande d’automates programmables Ladder Diagram, ainsi que par l’intégration d’un langage formel intermédiaire (FIACRE) dans la chaîne outillée de vérification. Ce dernier point permet de réduire l’écart sémantique entre les DSMLs et les domaines formels. / Domain specific Modeling Languages (DSMLs) are increasingly used at the early phases in the development of complex systems, in particular, for safety critical systems. The goal is to be able to reason early in the development on these models and, in particular, to fulfill verification and validation activities (V and V). A widely used technique is the exhaustive behavioral model verification using model-checking by providing a translational semantics to build a formal model from DSML conforming models in order to reuse powerful tools available for this formal domain. Defining a translational semantics, expressing formal properties to be assessed and analysing such verification results require such an expertise in formal methods that it restricts their adoption and may discourage the designers. It is thus necessary to build for each DSML, a toolchain which hides formal aspects for DSML end-users. The goal of this thesis consists in easing the development of such verification toolchains. Our contribution includes 1) expressing behavioral properties in the DSML level by relying on TOCL (Temporal Object Constraint Language), a temporal extension of OCL; 2) An automated transformation of these properties on formal properties while reusing the key elements of the translational semantics; 3) the feedback of verification results thanks to a higher-order transformation and a language which defines mappings between DSML and formal levels; 4) the associated process implementation. Our approach was validated by the experimentation on a subset of the development process modeling language SPEM, and on Ladder Diagram language used to specify programmable logic controllers (PLCs), and by the integration of a formal intermediate language (FIACRE) in the verification toolchain. This last point allows to reduce the semantic gap between DSMLs and formal domains.

Les applications réactives et sensibles au contexte sont des applications intelligentes qui observent l’environnement (ou contexte) dans lequel elles s’exécutent et qui adaptent, si nécessaire, leur comportement en cas de changements dans ce contexte, ou afin de satisfaire les besoins ou d'anticiper les intentions des utilisateurs. La recherche dans ce domaine suscite un intérêt considérable tant de la part des académiques que des industriels. Les domaines d'applications sont nombreux: robots industriels qui peuvent détecter les changements dans l'environnement de travail de l'usine pour adapter leurs opérations; systèmes de contrôle automobiles pour observer d'autres véhicules, détecter les obstacles, ou surveiller le niveau d'essence ou de la qualité de l'air afin d'avertir les conducteurs en cas d'urgence; systèmes embarqués monitorant la puissance énergétique disponible et modifiant la consommation en conséquence. Dans la pratique, le succès de la mise en œuvre et du déploiement de systèmes sensibles au contexte dépend principalement du mécanisme de reconnaissance et de réaction aux variations de l'environnement. En d'autres termes, il est nécessaire d'avoir une approche adaptative bien définie et efficace de sorte que le comportement des systèmes peut être modifié dynamiquement à l'exécution. En outre, la concurrence devrait être exploitée pour améliorer les performances et la réactivité des systèmes. Tous ces exigences, ainsi que les besoins en sécurité et fiabilité constituent un grand défi pour les développeurs.C’est pour permettre une écriture plus intuitive et directe d'applications réactives et sensibles au contexte que nous avons développé dans cette thèse un nouveau langage appelé INI. Pour observer les changements dans le contexte et y réagir, INI s’appuie sur deux paradigmes : la programmation événementielle et la programmation à base de règles. Événements et règles peuvent être définis en INI de manière indépendante ou en combinaison. En outre, les événements peuvent être reconfigurésdynamiquement au cours de l’exécution. Un autre avantage d’INI est qu’il supporte laconcurrence afin de gérer plusieurs tâches en parallèle et ainsi améliorer les performances et la réactivité des programmes. Nous avons utilisé INI dans deux études de cas : une passerelle M2M multimédia et un programme de suivi d’objet pour le robot humanoïde Nao. Enfin, afin d’augmenter la fiabilité des programmes écrits en INI, un système de typage fort a été développé, et la sémantique opérationnelle d’INI a été entièrement définie. Nous avons en outre développé un outil appelé INICheck qui permet de convertir automatiquement un sous-ensemble d’INI vers Promela pour permettre un analyse par model checking à l’aide de l’interpréteur SPIN. / Context-aware pervasive computing has attracted a significant research interest from both academy and industry worldwide. It covers a broad range of applications that support many manufacturing and daily life activities. For instance, industrial robots detect the changes of the working environment in the factory to adapt their operations to the requirements. Automotive control systems may observe other vehicles, detect obstacles, and monitor the essence level or the air quality in order to warn the drivers in case of emergency. Another example is power-aware embedded systems that need to work based on current power/energy availability since power consumption is an important issue. Those kinds of systems can also be considered as smart applications. In practice, successful implementation and deployment of context-aware systems depend on the mechanism to recognize and react to variabilities happening in the environment. In other words, we need a well-defined and efficient adaptation approach so that the systems' behavior can be dynamically customized at runtime. Moreover, concurrency should be exploited to improve the performance and responsiveness of the systems. All those requirements, along with the need for safety, dependability, and reliability pose a big challenge for developers.In this thesis, we propose a novel programming language called INI, which supports both event-based and rule-based programming paradigms and is suitable for building concurrent and context-aware reactive applications. In our language, both events and rules can be defined explicitly, in a stand-alone way or in combination. Events in INI run in parallel (synchronously or asynchronously) in order to handle multiple tasks concurrently and may trigger the actions defined in rules. Besides, events can interact with the execution environment to adjust their behavior if necessary and respond to unpredictable changes. We apply INI in both academic and industrial case studies, namely an object tracking program running on the humanoid robot Nao and a M2M gateway. This demonstrates the soundness of our approach as well as INI's capabilities for constructing context-aware systems. Additionally, since context-aware programs are wide applicable and more complex than regular ones, this poses a higher demand for quality assurance with those kinds of applications. Therefore, we formalize several aspects of INI, including its type system and operational semantics. Furthermore, we develop a tool called INICheck, which can convert a significant subset of INI to Promela, the input modeling language of the model checker SPIN. Hence, SPIN can be applied to verify properties or constraints that need to be satisfied by INI programs. Our tool allows the programmers to have insurance on their code and its behavior.