Contribution à une méthode outillée pour la conception de langages de modélisation métier interopérables, analysables et prouvables pour l'Ingénierie Système basée sur des Modèles

Systems Engineering (SE) is an interdisciplinary and collaborative approach for successful design and management of large scale complex systems. Among other principles, SE promotes and mandates a model-based (or model-driven) approach for all stages of system design processes, denoted Model-Based Systems Engineering (MBSE). This implies concepts, techniques and tools for creating and managing various systems models for the purpose of stakeholders, and for reaching and improving the quality of models helping then stakeholders during decision-making processes, to make decisions faster and efficiently with enough confidence. Indeed, these decisions impact all along the downstream phases of system engineering and development until the realization and deployment of the real system, its functioning, safety, security, induced costs and so on. In this work, a particular attention is given to model verification and validation (V&V). The goals are to assure prior to decision-making processes, first, that models are coherent, well-formed and correctly build and represented, and second, that they are trustworthy and relevant, representing as accurately as possible the viewpoints of a system under design as expected by stakeholders.Such models provide stakeholders with confidence and trust, aiding them in making, but also in arguing decisions. Models are created by using modeling languages that are specifically tailored for a given viewpoint of a system, denoted Domain Specific Modeling Languages (DSMLs).The basic principles on which a DSML is based are its syntax and its semantics, but current DSMLs have been more studied from the syntactical point than from the semantical one that is often neglected or, when needed, provided by means of translating the DSML into third party formalisms. This is the key limitation preventing the deployment of a successful V&V strategy in MBSE context. To overcome this shortcoming, this thesis proposes first a conceptual contribution consisting of a new metamodeling language, called eXecutable, Verifiable and Interoperable Core (xviCore), allowing stakeholders to build DSMLs (called xviDSMLs), that along with their syntax also integrates semantics. Our solution combines, three meta-languages, an object-oriented metamodeling language for the specification of the syntactical part with a formal behavioral modeling language and a property modeling language for the semantical part. The methodological contribution of this work allows the deployment of successful V&V strategies allowing for direct (without transformation) model verification by simulation and properties proof. We propose a mechanism to simulate the expected behavior of a SoI through model execution based on the blackboard-based communication model, and a mechanism for specification and verification of formal properties. The technical contribution consists of an Eclipse-EMF deployable plug-in that implements the metamodeling language xviCore and the mechanisms for simulation and formal property verification.L'Ingénierie des Systèmes (IS) est une approche pluridisciplinaire et collaborative pour mener à bâtir et structurer la conception puis la réalisation et le développement de systèmes complexes. L’IS repose à la fois sur une approche processus et sur la mise en oeuvre de modèles de systèmes s'appuyant de fait dans un contexte basé ou dirigé par des modèles. On parle alors d’Ingénierie Système Basée sur des Modèles (ISBM ou Model based Systems Engineering MBSE). L’ISBM introduit des concepts, méthodes et techniques pour construire et gérer des modèles. Elle a pour objectif l’atteinte et l’amélioration de leur qualité afin de procurer aux parties prenantes un degré de confiance jugé suffisant pour aider la prise des décisions de conception, d'amélioration et de réalisation. Ces décisions conditionnent le fonctionnement, la sûreté, la sécurité, les coûts, et plus généralement tout un ensemble de propriétés attendues à la fois du modèle comme du système modélisé, tout au long de la phase aval de l’ingénierie et de développement, jusqu’à la réalisation et au déploiement du système. La qualité des modèles est obtenue au travers des processus de Vérification et Validation (V&V). Les objectifs sont alors d’assurer que les modèles soient cohérents, bien formés, bien construits et représentés correctement. En effet, aux yeux des parties prenantes, les modèles doivent être fiables, fidèles et pertinents au regard des besoins des concepteurs, représentant aussi précisément que possible le point de vue du système en cours de conception. Des langages de modélisation dit « métier » (Domain Specific Modelling Languages ou DSML) sont spécifiquement créés pour pouvoir fournir des représentations i.e. des modèles dans les différents points de vue sur le système. Un DSML est basé sur une syntaxe et sur une sémantique. La sémantique de ces langages est en général fournie par des approches externes (vérificateurs de modèles). Ces dernières sont, à notre sens, une limitation clé pour le déploiement des stratégies de V&V dans le contexte de l’ISBM. En réponse à cette limitation, la contribution conceptuelle de cette thèse est présentée sous la forme d’un nouveau langage de métamodélisation, nommé xviCore (noyau exécutable, vérifiable et interopérable). xviCore fournit les concepts et les principes pour définir puis vérifier et valdier la syntaxe et la sémantique en phase de construction de tels DSML en combinant trois métalangages : un métalangage orienté objet pour la conception de la partie syntaxique, un métalangage pour la conception du comportement et un métalangage pour la conception de propriétés formelles. La contribution méthodologique de ces travaux permet ensuite le déploiement d’une stratégie de V&V «directe» en lieu et place des traditionnelles approches externes. Elle est basée sur la simulation et la preuve formelle de propriétés. Le mécanisme de simulation permet d’observer le comportement des modèles de systèmes au travers de leur exécution, tandis que le mécanisme de preuve permet de spécifier et ensuite de vérifier des propriétés formelles. La contribution technique se compose d’un ensemble des plugins Eclipse qui implémentent le métalangage xviCore, le mécanisme de simulation et le mécanisme de la preuve formelle