Dans cette thèse, nous abordons le problème de la modélisation et de la vérification de systèmes complexes présentant des comportements à la fois probabilistes et temporisés. La conception de tels systèmes est devenue de plus en plus complexe en raison de l’hétérogénéité des composants impliqués, l’incertitude découlant d’un environnement ouvert et les contraintes temps réelinhérentes à leurs domaines d’application. La gestion à la fois du logiciel et du matériel dans une vue unifiée tout en incluant des informations sur les performances (par exemple, temps de calcul et de communication, consommation d’énergie, etc.) devient indispensable. Construire et analyser des modèles de performance est d’une importance primordiale pour donner des garanties sur les exigences fonctionnelles et extra-fonctionnelles des systèmes, et permettre uneprise de décision fondée sur des mesures quantitatives dès les premières étapes de la conception.Cette thèse apporte plusieurs nouvelles contributions. Tout d’abord, nous introduisons un nouveau formalisme de modélisation appelé BIP stochastique et temps réel (SRT-BIP) pour la modélisation, la simulation et la génération de code de systèmes à base de composants. Ce formalisme hérite du framework BIP ses capacités de modélisation basées sur les composants et le temps réel et, en outre, il fournit des primitives pour exprimer des comportements stochastiquescomplexes.Deuxièmement, nous étudions des techniques d’apprentissage automatique pour faciliter la construction de modèles de performance. Nous proposons d’améliorer et d’adapter une procédure d’apprentissage présentée dans la littérature pour déduire des modèles stochastiques et temporisés à partir d’exécutions concrètes du système, et de les exprimer dans le formalisme SRT-BIP.Troisièmement, étant donné les modèles de performance dans SRT-BIP, nous explorons l’utilisation du model checking statistique (SMC) pour l’analyse d’exigences concernant la fonctionnalité et les performances du système. Pour ce faire, nous fournissons un framework complet, appelé SBIP, en tant qu’outil de support pour la modélisation, la simulation et l’analyse des systèmes SRT-BIP. SBIP est un environnement de développement intégré (IDE) qui implémente des algorithmes SMC pour des analyses quantitatives, qualitatives et d’événementsrares, en plus d’une procédure d’automatisation pour l’exploration des paramètres d’une propriété. Nous validons nos propositions sur des études de cas réels touchant à des domaines variés tels que les protocoles de communication, les systèmes concurrents et les systèmesembarqués.Enfin, nous étudions plus en détail l’intérêt du SMC lorsqu’il est inclus dans des méthodes d’analyse de système élaborées. Nous illustrons cela en proposant deux approches d’évaluation des risques. Dans la première approche, nous introduisons une méthodologie en spirale pour modéliser des systèmes résilients avec des composants FDIR que nous validons à travers l’évaluation de la sécurité du système de locomotion d’un rover d’exploration planétaire. La deuxième approche concerne l’évaluation des politiques de sécurité des organisations selon une approche de sécurité offensive. L’objectif est de synthétiser des configurations de défense efficaces contre des stratégies d’attaque optimisées (qui minimisent le coût d’attaque et maximisent la probabilité de succès). Ces stratégies d’attaque sont obtenues en combinant l’apprentissage de modèles et les méthodes méta-heuristiques, dans lesquels le SMC a le rôle principal d’évaluer et de prioriser les potentielles stratégies candidates. / In this thesis, we address the problem of modeling and verification of complex systems exhibiting both probabilistic and timed behaviors. Designing such systems has become increasingly complex due to the heterogeneity of the involved components, the uncertainty resulting from open environment and the real-time constraints inherent to their application domains. Handling both software and (abstraction of) hardware in a unified view while also including performanceinformation (e.g. computation and communication times, energy consumption, etc.) becomes a must. Building and analyzing performance models is of paramount importance in order to give guarantees on the functional and extra-functional system requirements and to make well-founded design decisions based on quantitative measures at early design stages.This thesis brings several new contributions. First, we introduce a new modeling formalism called Stochastic Real-Time BIP (SRT-BIP) for the modeling, the simulation and the code generation of component-based systems. This formalism inherits from the BIP framework its component-based and real-time modeling capabilities and, extends it by providing comprehensive primitives to express complex stochastic behaviors.Second, we investigate machine learning techniques to ease the construction of performance models. We propose to enhance and adapt a state-of-the-art learning procedure to infer stochastic real-time models from concrete system execution and to represent them in the SRT-BIP formalism.Third, given performance models in SRT-BIP, we explore the use of statistical Model Checking (SMC) for the anaysis of system’s functional and performance requirements. To do so, we provide a full framework, called SBIP, as a support tool for the modeling, simulation and analysis of SRT-BIP systems. SBIP is an Integrated Development Environment (IDE) that implements SMC algorithms for quantitative, qualitative and rare events analyses together with an automated exploring procedure for parameterized requirements. We validate our proposalson real-life case studies ranging from communication protocols and concurrent systems to embedded systems.Finally, we further investigate the interest of SMC when included in elaborated system analysis workflows. We illustrate this by proposing two risk assessment approaches. In the first approach, we introduce a spiral methodology to build resilient systems with FDIR components that we validate on the safety assessment of a planetary rover locomotion system. The second approach is concerned with the security assessment of organization’s defenses following an offensive security approach. The goal is to synthesize impactful defense configurations against optimized attack strategies (that minimize attack cost and maximize success probability). These attack strategies are obtained by combining model learning with meta heuristics, and where SMC is used to score and prioritize potential candidate strategies.

Dans le contexte actuel, la transformation de l’outil industriel par l’intermédiaire de nouveaux paradigmes de performance tels qu’Usine du Futur (Factory of the Future FoF), Industry 4.0 (I4.0) ou encore Smart Factory (SF) est au cœur des préoccupations actuelles des industriels. Les travaux présentés dans cette thèse portent sur la problématique de passage d’une situation spécifique existante (AS-IS) vers une situation cible type Usine du Futur (TO-BE) en prenant en compte la situation souhaitée AS-WISHED et les contraintes de ressources. Dans ce cadre, la principale contribution porte sur une approche reposant sur un modèle de co-évolution permettant de guider ce projet de transition au sein de l’organisation. Sur la base des travaux de Tolio et al. (2010), nous avons proposé un modèle de co-évolution amélioré en intégrant le niveau stratégique, le rôle du système d’information (SI) et celui de la place l’homme. Sur le plan théorique, le nouveau modèle de co-evolution aborde 3 domaines Produit/Production/SI qui sont structurés en deux niveaux d’analyse : externe (stratégique) et interne (structurel). L’ensemble de 6 sous-domaines comportent chacun 3 composants couvrant les choix relatifs à chaque sous-domaine et niveau d’analyse. Sur le plan managérial, la gestion de la co-évolution réside dans la modélisation des ces composants. Ensuite, nous caractérisons des liens de co-évolution existants entre les différents sous-domaines du modèle de co-évolution proposé. La démarche d’exploitation du modèle de co-évolution comporte trois étapes et considère les contraintes opérationnelles et les contraintes dites de co-évolution liées à la gestion des liens ou impacts entrant en jeu dans la co-évolution. Il permet de passer progressivement des modèles AS-IS et AS-WISHED pour aboutir à un modèle TO-BE. / Within the current context, the transformation of industries through new paradigms of performance such as The Factory of the Future (FoF), Industry 4.0 (I 4.0) or even The Smart Factory (SF) is at the heart of the industrials’ current concerns. The present work address the problem of the transition from a specific situation (AS-IS) to a target situation alike FoF (TO-BE) considering the desired situation AS-WISHED and the resources constraints. In this line of action, the main contribution concerns an approach based on a co-evolution model enabling to guide manufacturing industries to perform such a transition. Based on the work of Tolio et al. (2010), we propose an enhanced co-evolution model that integrates the strategic level of decisions, the information system role (IS) and the role of the human workforce. From the theoretical perspective, this new model consists in 3 domains: Product design/ Manufacturing/ IS which are structured into two levels of analysis: external (strategic) and internal (operational). The resulting structure of 6 sub-domains is in turn composed of 3 components covering the decisions related to each sub-domain and level of analysis. From the management perspective, the management of co-evolution relies on the modelling of their components. Hence, we exploit the modelling language constructs of the ISO 19440 (2007) standard for the internal components. Then, we characterize the existing co-evolution links between the different sub-domains of the proposed co-evolution model. At last, a 3 phase approach enabling to exploit the enhanced co-evolution model is proposed. It considers the feasibility constraints and the co-evolution constraints linked to the management of the links or impacts that came into play in the co-evolution. As such, it enables to work out progressively a feasible TO-BE model.