Vérification Formelle et Incrémentale de Spécifications SysML pour la Conception de Systèmes à Base de ComposantsLe travail présenté dans cette thèse est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisé avec le langage SysML. Les SBC sont largement utilisés dans le domaine industrielet ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l'utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en {\oe}uvre d'approches plus rigoureuses.Pour faciliter la communication entre les différentes parties impliquées dans le développement d'un SBC, un des langages largement utilisé est SysML, qui permet de modéliser, en plus de la structure et le comportement du système, aussi ses exigences. Il offre un standard de modélisation, spécification et documentation de systèmes, dans lequel il est possible de développer un système, partant d'un niveau abstrait, vers des niveaux plus détaillés pouvant aboutir à une implémentation. %Généralement ces systèmes sont faits plus grands parce qu'ils sont développés avec des cadres logiciels.Dans ce contexte nous avons traité principalement deux problématiques.La première est liée au développement par raffinement d'un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu'une composition d'un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d'un SBC. Dans cette contribution, nous exploitons les outils: Ptolemy pour la vérification de la compatibilité des composants assemblés, et l'outil MIO Workbench pour la vérification du raffinementLa deuxième problématique traitée concerne la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante: comment spécifier une architecture SBC qui satisfait toutes les exigences du système? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d'interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le model-checker SPIN et la LTL pour spécifier et vérifier les exigences.Mots clés: {Modélisation, Spécifications SysML, Architecture SBC, Raffinement, Compatibilité, Exigences, Propriétés LTL, Promela/SPIN, Ptolemy, MIO Workbench} / Formal and Incremental Verification of SysML Specifications for the Design of Component-Based SystemsThe work presented in this thesis is a contribution to the specification and verification of Component-Based Systems (CBS) modeled in SysML. CBS are widely used on the industrial field, and they are built by assembling various reusable components, allowing developing complex systems at lower cost.Despite the success of the use of CBS, their design is an increasingly complex step that requires the implementation of more rigorous approaches.To ease the communication between the various stakeholders in a CBS development project, one of the widely used modeling languages is SysML, which besides allowing modeling of structure and behavior, it has capabilities to model requirements. It offers a standard for modeling, specifying and documenting systems, wherein it is possible to develop a system, starting from an abstract level, to more detailed levels that may lead to an implementation.In this context, we have dealt mainly two issues. The first one concerns the development by refinement of a CBS, which is described only by its SysML interfaces and behavior protocols. Our contribution allows the designer of CBS to formally ensure that a composition of a set of elementary and reusable components refines an abstract specification of a CBS. In this contribution, we use the tools: Ptolemy for the verification of compatibility of the assembled components and MIO Workbench for refinement verification.The second one concerns the difficulty to decide what to build and how to build it, considering only system requirements and reusable components. Therefore, the question that arises is: how to specify a CBS architecture, which satisfies all system requirements? We propose a formal and incremental verification approach based on SysML models and interface automata to guide, by the requirements, the CBS designer to define a coherent system architecture that satisfies all proposed SysML requirements. In this approach we use the SPIN model-checker and LTL properties to specify and verify requirements.Keywords: {Modeling, SysML specifications, CBS architecture, Refinement, Compatibility, Requirements, LTL properties, Promela/SPIN, Ptolemy, MIO Workbench}

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

Le travail présenté dans cette thèse a lieu dans le domaine de développement basé sur les composants, il est une contribution à laspécification, l'adaptation et la vérification des systèmes à base de composants. Le but principal de cette thèse est la proposition d'uneapproche formelle pour construire progressivement des systèmes complexes en assemblant et en adaptant un ensemble de composants,où leur structure et leur comportement sont modélisés à l'aide de diagrammes SysML. Dans la première étape, nous avons défini uneapproche basée sur la méta-modélisation et la transformation des modèles pour vérifier la compatibilité des blocs ayant leurs protocolesd'interaction modélisés à l'aide de diagrammes de séquence SysML. Pour vérifier leur compatibilité, nous effectuons une transformationen automates d'interface (IAs), et nous utilisons l'approche optimiste définie sur les IA. Cette approche considère que deux composantssont compatibles s'il existe un environnement approprié avec lequel ils peuvent interagir correctement. Après cela, nous avons proposéde bénéficier de la hiérarchie, qui peut être présente dans les modèles de protocole d'interaction des blocs, pour alléger la vérification dela compatibilité des blocs. Dans l'étape suivante, nous avons pris en considération le problème des incohérences de noms de type one2oneentre les services des blocs. A ce stade, un adaptateur est généré pour un ensemble de blocs réutilisés qui ont leurs protocoles d'interactionmodélisés formellement par des automates d'interface. La génération de l'adaptateur est guidée par la spécification du bloc parent qui estfaite initialement par le concepteur. Notre approche est complétée par une phase de vérification qui nous permet de vérifier les exigencesSysML, exprimées formellement par les propriétés temporelles, sur les blocs SySML. Dans cette phase, nous avons exploité uniquementles adaptateurs générés pour vérifier la préservation des exigences initialement satisfaites par les blocs réutilisés. Ainsi, notre approchea l'intention de donner plus de chance d'éviter le problème de l'explosion de l'espace d'état au moment de la vérification. Dans le mêmecontexte, où nous avons un ensemble de blocs réutilisés et la spécification de leurs blocs parents, nous avons proposé d'utiliser des réseauxde Petri colorés (CPN) pour modéliser les interactions des blocs et générer des adaptateurs qui résolvent plus de types de problèmes. Dansce cas, l'adaptateur peut résoudre le problème de blocage en permettant le ré-ordonnancement des appels de services. / The work presented in this thesis takes place in the component-based development domain, it is a contribution to the specification,adaptation and verification of component-based systems. The main purpose of this thesis is the proposition of a formal approach tobuild incrementally complex systems by assembling and adapting a set of components, where their structure and behaviour are modelledusing SysML diagrams. In the first stage, we have defined a meta-model driven approach which is based on meta-modelling and modelstransformation, to verify the compatibility of blocks having their interaction protocols modelled using SysML sequence diagrams. To verifytheir compatibility, we perform a transformation into interface automata (IAs), and we base on the optimistic approach defined on IAs. Thisapproach consider that two components are compatible if there is a suitable environment with which they can interact correctly. Afterthat, we have proposed to benefit from the hierarchy, that may be present in the interaction protocol models of the blocks, to alleviate theverification of blocks compatibility. In the next stage, we have taken into consideration the problem of names mismatches of type one2onebetween services of blocks. At this stage, an adapter is generated for a set of reused blocks which have their interaction protocols modelledformally by interface automata. The generation of the adapter is guided by the specification of the parent block which is made initiallyby the designer. Our approach is completed by a verification phase which allows us to verify SysML requirements, expressed formallyby temporal properties, on SySML blocks. In this phase, we have exploited only the generated adapters to verify the preservation of therequirements initially satisfied by the reused blocks. Thus, our approach intends to give more chance to avoid the state space explosionproblem during the verification. In the same context, where we have a set of reused blocks and the specification of their parent blocks, wehave proposed to use coloured Petri nets (CPNs) to model the blocks interactions and to generate adapters that solve more type of problems.In this case the adapter can solve the problem of livelock by enabling the reordering of services calls.

La sécurité-innocuité est une propriété émergente des systèmes critiques de sécurité (SCS), notamment les systèmes ferroviaires. Cet aspect émergent complexifie leur processus du développement et nécessite un raisonnement judicieux permettant de diminuer les dangers. Cette thèse propose une approche ontologique qui intègre les activités de sécurité dès les premières phases de conception des SCS. Ce cadre structuré offre une harmonisation sémantique entre les domaines impliqués, tels que l'ingénierie de sécurité et l'Ingénierie des Exigences Dirigée par les Buts (IEDB). La logique métier intégrée dans cette approche est validée par des cas d'étude ferroviaires d'accidents réels et d'une mission télé-opérée. Dans un premier temps, nous avons proposé une ontologie d'analyse dysfonctionnelle appelée DAO et fondée sur l'ontologie de haut niveau UFO. DAO considère les aspects sociaux-techniques et environnementaux des SCS et intègre les différents types de fautes et de propriétés cognitives liés respectivement aux défaillances techniques et aux erreurs humaines. Le modèle conceptuel de DAO est exprimé en OntoUML et formalisé en langage OWL afin de fournir un support de raisonnement. Ensuite, un pont sémantique est établi entre les mesures de sécurité, les buts de sécurité et les exigences de sécurité par le développement d'une ontologie de gestion de sécurité orientée-but, appelée GOSMO. La gestion des décisions de sécurité s’appuie sur la réinterprétation du modèle de contrôle d'accès Or-Bac d'un point de vue sécurité-innocuité. Afin d'assurer la cohérence globale des exigences, GOSMO permet de structurer la gestion des évolutions des exigences et leur traçabilité. / Safety is an emergent property of safety critical systems (SCS), including railway systems. This emergent aspect exacerbates their development process and requires a thorough reasoning to reduce hazards. This thesis proposes an ontological approach that integrates safety activities from the early design stages of SCS. This structured framework provides a semantic harmonization between the involved domains, such as safety engineering and Goal Oriented Requirements Engineering (GORE). The business logic integrated in this approach is validated by real rail accident scenarios and a remotely operated task. At first, we proposed a dysfunctional analysis ontology called DAO and based on the high-level ontology UFO. DAO considers the socio-technical and environmental aspects of SCS and integrates the different types of faults and cognitive properties that are respectively related to technical failures and human errors. The DAO conceptual model is expressed in OntoUML and formalized in OWL language in order to provide a reasoning support. Then, a semantic bridge is established between safety measures, safety goals and safety requirements through the development of a goal-oriented security management ontology, called GOSMO. The management of safety decisions is based on the reinterpretation of the Or-Bac access control model from a safety point of view. In order to ensure the overall consistency of requirements, GOSMO allows structuring the management of requirements changes and their traceability

La complexité des systèmes conçus actuellement devient de plus en plus importante. En effet,afin de rester compétitives, les entreprises concevant des systèmes cherchent à leur rajouter de plus en plusde fonctionnalités. Cette compétitivité introduit aussi une demande de réactivité lors de la conception desystèmes, pour que le système puisse évoluer lors de sa conception et suivre les demandes du marché.Un des éléments identifiés comme empêchant ou diminuant cette capacité à concevoir de manière flexibledes systèmes complexes concerne les spécifications des systèmes, et en particulier l’utilisation de la languenaturelle pour spécifier les systèmes. Tout d’abord, la langue naturelle est intrinsèquement ambiguë et celarisque donc de créer des non-conformités si client et fournisseur d’un système ne sont pas d’accord sur lesens de sa spécification. De plus, la langue naturelle est difficile à traiter automatiquement, par exemple, onpeut difficilement déterminer avec un programme informatique que deux exigences en langue naturelle secontredisent. Cependant, la langue naturelle reste indispensable dans les spécifications que nous étudions,car elle reste un moyen de communication pratique et très répandu.Nous cherchons à compléter ces exigences en langue naturelle avec des éléments permettant à la fois de lesrendre moins ambiguës et de faciliter les traitements automatiques. Ces éléments peuvent faire partie demodèles (d’architecture par exemple) et permettent de définir le lexique et la syntaxe utilisés dans lesexigences. Nous avons testé les principes proposés sur des spécifications industrielles réelles et développéun prototype logiciel permettant de réaliser des tests sur une spécification dotée de ces éléments de syntaxeet de lexique. / Systems are becoming more and more complex, because to stay competitive, companies whichdesign systems search to add more and more functionalities to them. Additionally, this competition impliesthat the design of systems needs to be reactive, so that the system is able to evolve during its conception andfollow the needs of the market.This capacity to design flexibly complex systems is hindered or even prevented by various variouselements, with one of them being the system specifications. In particular, the use of natural language tospecify systems have several drawbacks. First, natural language is inherently ambiguous and this can leadsto non-conformity if customer and supplier of a system disagree on the meaning of its specification.Additionally, natural language is hard to process automatically : for example, it is hard to determine, usingonly a computer program, that two natural language requirements contradict each other. However, naturallanguage is currently unavoidable in the specifications we studied, because it remains very practical, and itis the most common way to communicate.We aim to complete these natural language requirements with elements which allow to make them lessambiguous and facilitate automatic processing. These elements can be parts of models (architectural modelsfor example) and allow to define the vocabulary and the syntax of the requirements. We experimented theproposed principles on real industrial specifications and we developped a software prototype allowing totest a specification enhanced with these vocabulary and syntax elements.

Depuis la loi interdisant la dissimulation du visage dans l’espace public adoptée le 11 octobre 2010 jusqu’à aujourd’hui, la tension entre la liberté religieuse et les valeurs de la République est prégnante. Les valeurs de la République, qui renvoient stricto sensu à la devise « Liberté, Égalité, Fraternité », sont conjuguées avec d’autres notions. Dans le processus d’élaboration de la loi de 2010, elles sont articulées à la dignité et l’égalité des sexes. Depuis, elles sont conjuguées avec, voire identifiées à la laïcité, érigée en valeur, et les citoyens sont appelés à adhérer à cet ensemble axiologique. Cette évolution des cadres de référence dans la prise en compte du religieux par l’État, et la tension qu’elle emporte entre la liberté religieuse et les valeurs de la République, doivent être interrogées. / On October 11th, 2010, a Frenchlaw prohibits the deliberate concealment of hiding the face in public spaces. Since then, the tensions between freedom of religion and the values of the Republic remain strong. Theses republican values which strictly refer to the motto « Liberty, Equality, Fraternity » coexist with many concepts. During the process of law-making, the bill articulated the French Republic values with dignity and gender equality. Ever since these newly added concepts are now accepted as components of the secularism. Citizens are called to adhere to this value system. The framework evolution required by the consideration of the religious fact of the State and the strong tensions between the freedom of religion and the values of Republic must be analyzed.

Le langage est dans son ensemble bien préservé pendant le vieillissement (Meyer & Federmeier, 2010) tandis que la mémoire sémantique peut même s'améliorer (Kavé, Samuel-Enoch, & Adiv, 2009; Prinz, Bucher, & Marder, 2004; Salthouse, 2009; Verhaegen & Poncelet, 2013 ; Wingfield & Grossman, 2006), malgré de nombreux changements neurophysiologiques se produisant dans le cerveau (Grady, Springer, Hongwanishkul, McIntosh, & Winocur, 2006 ; Kemper & Anagnopoulos, 1989 ; Wingfield & Grossman, 2006). Cette thèse se concentre sur la préservation de la mémoire sémantique dans le vieillissement, « l'acte cognitif d'accéder aux connaissances stockées sur le monde » (Binder, Desai, Graves et Conant, 2009) à travers une tâche de jugement sémantique manipulant le contrôle sémantique avec deux niveaux de demande (faible et élevé) et deux types de relations sémantiques (taxonomique et thématique). Nous avons développé une nouvelle tâche variant les niveaux de demande (faible et élevé) chez 39 adultes jeunes et 39 adultes âgés. Plus précisément, les objectifs de notre étude étaient 1) d'identifier si le vieillissement affecte l'activité cérébrale liée à la mémoire sémantique conformément aux prédictions du modèle CRUNCH, à travers une tâche de jugement sémantique à deux niveaux d'exigences. 2) de combler le vide de la littérature sur l'existence et l'évolution des hubs sémantiques dans le vieillissement, à la lumière des théories single hub et dual-hub, en évaluant l'effet du vieillissement sur le rôle des lobes temporaux antérieurs (ATL) et du jonction temporo-pariétale (TPJ) en tant que représentations neuronales des centres sémantiques responsables respectivement du traitement taxonomique et thématique. Une soumission par rapport pré-enregistré (registered report) a été utilisée pour ce projet de recherche. Nos participants, adultes plus jeunes et plus âgés, étaient globalement appariés en termes de réserve cognitive, plus précisément en ce qui concerne le niveau d'éducation et comme le montrent les questionnaires évaluant l'engagement dans des activités cognitivement stimulantes, les tests MoCA et WAIS-III. Les résultats comportementaux ont confirmé que la tâche varie correctement la difficulté de la tâche puisque les taux d'erreur et les temps de réponse (RT) augmentent de manière linéaire avec l'augmentation des exigences de la tâche, à savoir dans la condition de forte demande. Nous avons constaté que la participation à des activités stimulantes sur le plan cognitif avait un impact positif à la fois sur les RT de référence et sur la précision. Nous n’avons pas observé de différence statistiquement significative dans la précision entre les participants jeunes et plus âgés, quelle que soit la condition. Nous avons constaté que des scores plus élevés aux tests WAIS-III et PPTT étaient positivement corrélés avec la précision chez les personnes âgées. En termes de RT, nous avons observé une différence statistiquement significative entre les participants jeunes et plus âgés pour la tâche et les conditions de référence, les adultes plus âgés étant plus lents à répondre en général. Les RT augmentent linéairement avec l'âge du participant. En tant que telle, la tâche de mémoire sémantique a réussi à a) manipuler la difficulté de la tâche sur deux niveaux d'exigences et b) démontrer une performance comportementale invariante selon l'âge pour le groupe plus âgé, comme l'exige le test du modèle CRUNCH (Fabiani, 2012 ; Schneider-Garces et al., 2010). Pour l'objectif n°1, les tests cruciaux du modèle CRUNCH, l'interaction IRMf groupe par difficulté, n'étaient pas cohérents avec les prédictions du modèle. Malgré nos résultats comportementaux, lorsque nous avons comparé directement la condition de faible demande avec la condition de forte demande, il n'y avait pas de différence statistiquement significative dans l'activation entre les conditions de faible et de forte demande. Nous n'avons pas non plus obtenu d'interaction entre tranche d'âge et difficulté. Nous avons obtenu des interactions significatives en comparant les conditions de demande faible et élevée avec la ligne de référence. Au niveau neuronal, indépendamment de l'âge, la tâche de jugement de similarité sémantique a activé un large réseau bilatéral fronto-temporo-pariétal. Pour l'objectif n°2 concernant l'effet de relation sémantique, le contraste de la condition taxonomique avec la condition thématique directement n'a pas trouvé d'activation robuste à un seuil corrigé. La condition taxonomique a donné des résultats intéressants par rapport à la condition de base. Sept groupes distincts dans le cortex fronto-temporo-pariétal ont été activés dans les deux hémisphères, y compris les lobes temporaux antérieurs (ATL) et la jonction temporo-pariétale gauche (TPJ). De plus, l'activation était significative dans le gyrus supérieur frontal gauche, le gyrus angulaire gauche (AG) et le gyrus frontal inférieur (partie orbitale) sur l'hémisphère droit. Cette découverte pourrait être en partie conforme à la théorie du double-hub, qui propose que les ATL bilatéralement et le TPJ agissent comme des hubs sémantiques. Bien que nous n'ayons pas trouvé d'activation significative dans les ATL pendant la condition taxonomique et dans le TPJ pendant la condition thématique, nous avons cependant constaté que dans la condition taxonomique parmi les sept clusters significativement activés, l'activation dans le gyrus frontal supérieur gauche était significativement corrélée avec la performance dans la condition taxonomique pour les deux groupes d'âge. L'activation dans le gyrus temporal moyen droit était également corrélée à l'amélioration des performances, mais cela n'était pas significatif dans le groupe plus âgé. En ce qui concerne la condition thématique, par contraste avec condition de référence, dix groupes distincts ont été activés, y compris la jonction temporo-pariétale (TPJ), alors que les ATL n'ont pas été activés de manière robuste pendant la condition thématique. Plus précisément, les régions activées comprenaient bilatéralement le gyrus angulaire, le gyrus temporal moyen, le gyrus frontal inférieur (partie triangulaire) et le gyrus frontal moyen. Nous visons à poursuivre des analyses supplémentaires pour explorer la relation entre les exigences de la tâche, le type de relation sémantique et la réorganisation neurofonctionnelle liée à l'âge. Cependant, ces résultats relatifs à la préservation avec l'âge des capacités à traiter les différentes relations sémantiques de mots sont associés à un certain nombre de réorganisations neurofonctionnelles. Celles-ci peuvent être spécifiques au traitement de différentes relations sémantiques et de différentes demandes de tâches. Il reste à déterminer si cette réorganisation est induite par les changements structurels du cerveau avec l'âge, ou par l'utilisation accrue de telles relations sémantiques tout au long de la trajectoire de la vie. / Language overall is well preserved in aging (Meyer & Federmeier, 2010) whereas semantic memory may even improve (Kavé, Samuel-Enoch, & Adiv, 2009; Prinz, Bucher, & Marder, 2004; Salthouse, 2009; Verhaegen & Poncelet, 2013; Wingfield & Grossman, 2006), despite numerous neurophysiological changes taking place in the brain (Grady, Springer, Hongwanishkul, McIntosh, & Winocur, 2006; Kemper & Anagnopoulos, 1989; Wingfield & Grossman, 2006). The present study focuses on the preservation of semantic memory in aging, the ‘cognitive act of accessing stored knowledge about the world’ (Binder, Desai, Graves, & Conant, 2009) by means of a semantic judgment task manipulating semantic control with two demand levels (low and high) and two types of semantic relations (taxonomic-thematic). We used a novel task that varied task demands (low versus high) in 39 younger and 39 older adults. More specifically, the aims of this study was 1) to identify whether aging affects the brain activity subserving semantic memory in accordance with the CRUNCH predictions, through a semantic judgment task with two levels of demands (low and high). 2) To bridge the gap in the literature on the existence and evolution of semantic hubs in aging, in light of the dual and single-hub theories, by evaluating the effect of aging on the role of the Anterior Temporal Lobes (ATLs) and the Temporo-parietal junction (TPJ) as neural representations of the semantic hubs responsible for taxonomic and thematic processing, respectively. A submission by registered report was opted for this research project. Our participants, younger and older adults, were overall matched in regards to level of education and as shown in questionnaires assessing engagement in cognitively stimulating activities, MoCA and WAIS-III tests. The behavioral results confirmed that the task was successful in manipulating task difficulty, with error rates and RTs increasing with increasing task demands, namely in the high-demand condition. We found that engaging in cognitively stimulating activities impacted positively on both baseline RTs and accuracy and that higher scores on the WAIS-III and the PPTT tests were positively correlated with accuracy in older adults. There was no statistical difference in accuracy between younger and older participants regardless of the condition, so there was no age effect in accuracy. In terms of RTs, there was a statistically significant difference between younger and older participants for both the task and the baseline conditions, with older adults being slower to respond in general. RTs increased the more the participant’s age increased, which is in line with findings in the literature. As such, the semantic memory task was successful in a) manipulating task difficulty across two levels of demands and b) demonstrating age-invariant behavioural performance for the older group, as requires to test the CRUNCH model (Fabiani, 2012; Schneider-Garces et al., 2010). For objective no 1, the crucial test of CRUNCH model, the fMRI age group by task demand interaction was not found. We did not find statistically significant interaction neither between task demands and age group for RTs or accuracy, nor in regards to brain activation. At the neural level, independently of age, the semantic similarity judgment task activated a large network including bilateral inferior frontal, parietal, supplementary motor, temporal and occipital brain regions, which correspond overall with the semantic network, as suggested in the literature. Region of interest analyses demonstrated task demand effect in these regions, most notably in the left and right inferior frontal gyrus, the left posterior middle temporal gyrus, the posterior inferior temporal gyrus and the pre-frontal gyrus, regions which are typically associated with semantic control requirements. We did not find any significant interactions between task demands and activation in the regions of interest either. Several possible reasons may justify the lack of findings as predicted by the CRUNCH hypothesis. For objective no 2 in regards to the semantic relation effect, the contrast of the taxonomic with the thematic condition directly did not produce any robust activation at a corrected threshold. The taxonomic condition yielded interesting results when contrasted with the baseline one. Seven distinct clusters in the fronto-temporo-parietal cortex were activated across the two hemispheres, including the anterior temporal lobes (ATLs) and the left temporo-parietal junction (TPJ). Additionally, activation was significant in the left frontal syperior gyrus, the left angular gyrus (AG) and the inferior frontal gyrus (orbital part) on the right hemisphere. This finding could be partly in line with the dual-hub theory, that proposes that the ATLs bilaterally and the TPJ act as semantic hubs. Though we did not find the expected double dissociation e.g., significant activation in the ATLs during the taxonomic condition only and in the TPJ during the thematic condition only, we found however that in the taxonomic condition among the seven significantly activated clusters, activation in the left superior frontal gyrus was significantly correlated with performance in both age groups. Activation in the right middle temporal gyrus was also correlated with improved performance, but this was not significant in the older group. During the thematic condition, when contrasted with baseline, ten distinct clusters were activated, including the temporo-parietal junction (TPJ), whereas the ATLs were not robustly activated during the thematic condition. We aim to pursue additional analyses to explore the relation between task demands, type of semantic relation and age-related neurofunctional reorganization. However, these results in relation to the preservation with age of the abiliites to process the different semantic word relations is associated with a number of neurofunctional reorganizations. These can be specific to the processing of different semantic relations and different task demands. Whether this reorganization is induced by the structural changes in the brain with age, or by the enhanced use of such semantic relations along the trajectory of life is still under exploration.

L'industrie automobile des systèmes embarqués critiques est confrontée de nos jours à une complexité croissante, tandis que les coûts, les performances en termes d'intelligence, les caractéristiques, les capacités et les délais de commercialisation de leurs produits sont constamment remises en question. Face à cela, l'objectif principal pour les constructeurs et fournisseurs automobiles devient désormais de contrôler la qualité et la fiabilité des systèmes mécatroniques et embarqués. L'existence de normes internationales comme le HIS Automotive SPICE et l’ISO26262 est une contrainte supplémentaire qu'ils doivent prendre en compte s’ils veulent atteindre cet objectif. De plus, assurer la bonne gestion de la sécurité et la qualité du produit ne suffit pas: il est essentiel de veiller à ce que nous produisons un système qui n'est pas seulement sécuritaire et bien, mais aussi que nous produisons le bon système. Cela induit donc une plus grande prise en compte des exigences.Dans cette thèse, nous traitons le challenge du développement des systèmes embarqués automobiles suivant l’Ingénierie Dirigée par les Modèles (IDM) qui répondent aux exigences des utilisateurs et des standards du domaine et qui permettent de maîtriser davantage la qualité des produits développés. Le problème à résoudre a été abordé sur plusieurs phases qui sont ensuite utilisés conjointement. En premier, nous définissons un métamodèle fusionnant les approches orienté qualité produit et qualité processus selon respectivement les normes ISO26262 et SPICE. Puis, dans un but de certification, nous proposons une méthodologie générique basée sur ce métamodèle commun où une évaluation du processus de développement induite par l’HIS standard ainsi qu’une évaluation de la sécurité fonctionnelle induite par l’ISO2626 sont simultanément effectuées. Ce résultat est traduit au travers de la définition d'un framework outillé où nous appliquons la méthode d'évaluation propre au standard SPICE. En deuxième phase, nous définissons un métamodèle pour gérer les actifs de sécurité concernant ces normes automobiles au niveau produit. Ce métamodèle définit comment capturer les exigences et l’architecture d’un système de telle manière qu'ils puissent être traçables entre eux et également traçables depuis des documents de spécifications d’origine. Enfin, une approche à base de modèle où l'interaction des modèles de processus et le produit est géré afin de répondre aux besoins identifiés dans la première phase est développé pour soutenir la gestion de projet. L'approche utilise la modélisation des processus et leur mesure pour améliorer le contrôle et le suivi de projet et de réduire par la même les coûts et les fréquences de replanification.Les avantages de la contribution sont démontrés sur une application pilote automobile, validant ainsi le travail de recherche au vue des faiblesses identifiées préalablement dans le contexte. / The embedded safety-critical systems industry is facing an exponential increase in the complexity and variety of systems and devices while costs, performance in terms of intelligence, features, capacities and time to market are constantly challenged. The main objective for automotive manufacturers and suppliers is now becoming the control of quality and the dependability of embedded and mechatronic systems. The existence of internationally recognized standards such as the Automotive SPICE and ISO26262 is a further constraint that must be managed to meet this objective. Nevertheless, ensuring sound management of safety and viewpoints is insufficient. It is also essential to ensure that we produce a system that is not only compliant and well-defined, but also that we produce the “right” system. Therefore, this leads to greater consideration of the requirements.In this thesis, we address the challenge of development of automotive embedded systems following the model-driven engineering paradigm that meet the user needs and the regulatory constraints of the domain and that further mastered the quality of developed product. We resolve the problem in many steps which are subsequently used jointly. In the first phase, we define a merging approach which embodies a product quality and process quality approaches regarding the ISO26262 and SPICE standards following the model-driven engineering paradigm. Then, in a certification assessment purpose, we propose a generic methodology where an HIS assessment and a functional safety audit is simultaneously performed without altering their original meanings. This commitment results into the definition of a tooled framework where we apply the SPICE assessment method to the common metamodel defined from the merging work. In a second phase, we define a metamodel for manage safety assets regarding these automotive standards at product level. This metamodel defines how the requirements and architecture of a system can be captured in such a way that they can be traceable from each other and from origin specifications documents. Finally, a model-based approach where the interaction of process and product models is managed to address requirements identified in the precedent phases is developed to support project management. The approach uses process modeling and measurement to improve the control and the monitoring of project and to reduce the cost and frequency of re-planning.The benefits of the contribution are demonstrated on an ongoing automotive pilot application, thereby validating the research work against the weaknesses identified prealably in the context.

L'ingénierie des systèmes complexes et systèmes de systèmes conduit souvent à des activités de modélisation (MA) complexes. Les problèmes soulevés par les MA sont notamment : comprendre le contexte dans lequel elles sont exécutées, comprendre l'impact sur les cycles de vie des modèles qu'elles produisent, et finalement trouver une approche pour les maîtriser. L'objectif principal de cette thèse est d'élaborer une approche formelle pour adresser ce problème. Dans cette thèse, après avoir étudié les travaux connexes en ingénierie système et plus spécifiquement ceux qui portent sur la co-ingénierie du système à faire (le produit) et du système pour faire (le projet), nous développons une méthodologie nommée MODEF pour traiter ce problème. MODEF consiste en: (1) Caractériser les MA comme un système et plus généralement une fédération de systèmes. (2) Construire de manière itérative une architecture de ce système via la modélisation du contenu conceptuel des modèles produits par MA et leur cycle de vie, les tâches réalisées au sein des MA et leurs effets sur ces cycles de vie. (3) Spécifier les attentes sur ces cycles de vie. (4) Analyser les modèles (des MA) par rapport à ces attentes (et éventuellement les contraintes sur les tâches) pour vérifier jusqu'à quel point elles sont atteignables via la synthèse des points (ou états) acceptables. D'un point de vue pratique, l'exploitation des résultats de l'analyse permet de contrôler le déroulement des tâches de modélisation à partir de la mise en évidence de leur impact sur les modèles qu'elles produisent. En effet, cette exploitation fournit des données pertinentes sur la façon dont les MA se déroulent et se dérouleraient de bout en bout. A partir de ces informations, il est possible de prendre des mesures préventives ou correctives. Nous illustrons cela à l'aide de deux cas d'étude (le fonctionnement d'un supermarché et la modélisation de la couverture fonctionnelle d'un système). D'un point de vue théorique, les sémantiques formelles des modèles des MA et le formalisme des attentes sont d'abord données. Ensuite, les algorithmes d'analyse et d'exploitation sont présentés. Cette approche est brièvement comparée avec des approches de vérification des modèles et de synthèse de systèmes. Enfin, deux facilitateurs de la mise en œuvre de MODEF sont présentés. Le premier est une implémentation modulaire des blocs de base de MODEF. Le second est une architecture fédérée (FA) des modèles visant à faciliter la réutilisation des modèles formels en pratique. La formalisation de FA est faite dans le cadre de la théorie des catégories. De ce fait, afin de construire un lien entre abstraction et implémentation, des structures de données et algorithmes de base sont proposés pour utiliser FA en pratique. Différentes perspectives sur les composantes de MODEF concluent ce travail. / The engineering of complex systems and systems of systems often leads to complex modelling activities (MA). Some challenges exhibited by MA are: understanding the context where they are carried out and their impacts on the lifecycles of models they produce, and ultimately providing a support for mastering them. How to address these challenges with a formal approach is the central challenge of this thesis. In this thesis, after discussing the related works from systems engineering in general and the co-engineering of the system to be made (product) and the system for make (project) systems specifically, we position and develop a methodology named MODEF, that aims to master the operation of MA. MODEF consists in: (1) characterizing MA as a system (and more globally as a federation of systems) in its own right; (2) iteratively architecting this system through: the modelling of the conceptual content of the models produced by MA and their life cycles, the tasks carried out within MA and their effects on these life cycles; (3) specifying the expectations over these life cycles and; (4) analysing models (of MA) against expectations (and possibly tasks constraints) - to check how far expectations are achievable - via the synthesis of the acceptable behaviours. On a practical perspective, the exploitation of the results of the analysis allows figuring out what could happen with the modelling tasks and their impacts on the whole state of models they handle. We show on two case studies (the operation of a supermarket and the modelling of the functional coverage of a system) how this exploitation provides insightful data on how the system is end-to-end operated and how it can behave. Based on this information, it is possible to take some preventive or corrective actions on how the MA are carried out. On the foundational perspective, the formal semantics of three kinds of involved models and the expectations formalism are first discussed. Then the analysis and exploitation algorithms are presented. Finally this approach is roughly compared with model checking and systems synthesis approaches. Last but not least, two enablers whose first objectives are to ease the implementation of MODEF are presented. The first one is a modular implementation of MODEF's buildings blocks. The second one is a federated architecture (FA) of models which aims to ease working with formal models in practice. Despite the fact that FA is formalised within the abstract framework of category theory, an attempt to bridge the gap between abstraction and implementation is sketched via some basic data structures and base algorithms. Several perspectives related to the different components of MODEF conclude this work.

Cette thèse est composée de trois articles d’économie bancaire empirique. Le premier article traite de l’impact des conditions d’octroi de crédit sur l’accession à la propriété et les prix immobilier. Il propose une stratégie d’identification d’effets de causalité utilisant la politique du Prêt à Taux Zéro. Il conclut qu’un relâchement des conditions d’octroi de crédit permet à des ménages au revenu relativement plus faible de devenir propriétaire mais augmente significativement les prix immobilier. Le second article traite de l’effet des exigences en capital sur l’octroi de crédit des banques aux sociétés non financières. Il isole la composante des exigences en capital exogène aux conditions macroéconomiques grâce au système de notation du superviseur bancaire français. Il montre que les mesures de la qualité de la gouvernance et de la stratégie des établissements sont des contributeurs importants aux exigences en capital. En traçant l’effet de celles-ci sur les ratios de capital des établissements puis sur l’octroi de crédit, il montre qu’augmenter les exigences en capital réduit l’offre de crédit. Le troisième article analyse la prise en compte du risque de crédit sur le marché interbancaire européen entre 2011 et 2015 et comment celle-ci est modifiée par les ajustements de la politique monétaire sur la période. Il se concentre sur le risque inhérent à la détention d’actifs situés dans les pays périphériques de la zone euro. Il montre que l’accès au marché et les taux d’intérêt payés par les emprunteurs réagissent à cette détention. La nature et l’importance de cette réaction dépendent des interventions de politique monétaire. / This thesis is made up of three empirical essays in banking economics. The first paper analyses how credit supply conditions impact access to homeownership and real estate prices.We propose an identification strategy of causal effects based on the French Interest-Free Loan policy. We find loosenning credit conditions allows households with a relatively lower income to access homeownership but significantly increases real estate prices. The second paper looks for the effect of capital requirements on credit supply to non-financial companies.We identify movements in capital requirements exogenous to the macroeconomic environment thanks to the French banking supervisor rating system. We show governance and strategy quality measures significantly contribute to capital requirements setting. Followingtheir effects onto banks capital ratios and credit supply, we show raising capital requirementsreduces credit. The third article analyses credit risk management on the European interbankmarket between 2011 and 2015 and how it is modified by monetary policy adjustments overthe period. We focus on credit risk associated with holdings of assets located in peripheral Europe countries. We show market access and interest rates served to borrowers react to their holdings of such assets. The direction and size of this reaction depends on monetary policy interventions.