Nos tutelles

CNRS

Nos partenaires


Accueil > Publications > Thèses > Archives Thèses > Thèses 2016 - 2017

ALIYU Ahmzat


"An Integrative Framework for Model-Driven Systems Engineering - Towards the Co-Evolution of Simulation, Formal Analysis and Enactment Methodologies for Discrete Event Systems"

Les méthodes d’ingénierie dirigée par modèle des systèmes, telles que la simulation, l’analyse formelle et l’émulation ont été intensivement utilisées ces dernières années pour étudier et prévoir les propriétés et les comportements des systèmes complexes. Les résultats de ces analyses révèlent des connaissances qui peuvent améliorer la compréhension d’un système existant ou soutenir un processus de conception de manière à éviter des erreurs couteuses (et catastrophiques) qui pourraient se produire dans le système. Les réponses à certaines questions que l’on se pose sur un système sont généralement obtenues en utilisant des méthodes d’analyse spécifiques ; par exemple les performances et les comportements d’un système peuvent être étudiés de façon efficace dans certains cadres expérimentaux, en utilisant une méthode appropriée de simulation. De façon similaire, la vérification de propriétés telles que la vivacité, la sécurité et l’équité sont mieux étudiées en utilisant des méthodes formelles appropriées tandis que les méthodologies d’émulation peuvent être utilisées pour vérifier des hypothèses temporelles et des activités et comportements impliquant des interactions humaines. Donc, une étude exhaustive d’un système complexe (ou même d’apparence simple) nécessite souvent l’utilisation de plusieurs méthodes d’analyse pour produire des réponses complémentaires aux probables questions. Nul doute que la combinaison de multiples méthodes d’analyse offre plus de possibilités et de rigueur pour analyser un système que ne peut le faire chacune des méthodes prise individuellement. Si cet exercice (de combinaison) permet d’aller vers une connaissance (presque) complète des systèmes complexes, son adoption pratique ne va pas de pair avec les avancées théoriques en matière de formalismes et d’algorithmes évolués, qui résultent de décennies de recherche par les praticiens des différentes méthodes. Ce déficit peut s’expliquer par les compétences mathématiques requises pour utiliser ces formalismes, en combinaison avec la faible portabilité des modèles entre les outils des différentes méthodes. Cette dernière exigence rend nécessaire la tâche herculéenne de créer et de gérer plusieurs modèles du même système dans différents formalismes et pour différents types d’analyse. Un autre facteur bloquant est que la plupart des environnements d’analyse sont dédiés à une méthode d’analyse spécifique (i.e., simulation, ou analyse formelle, ou émulation) et sont généralement difficiles à étendre pour réaliser d’autres types d’analyse. Ainsi, une vaste connaissance de formalismes supportant la multitude de méthodes d’analyse est requise, pour pouvoir créer les différents modèles nécessaires, mais surtout un problème de cohérence se pose lorsqu’il faudra mettre à jour séparément ces modèles lorsque certaines parties du système changent. La contribution de cette thèse est d’alléger les charges d’un utilisateur de méthodes d’analyse multiples, dans sa quête d’exhaustivité dans l’étude des systèmes complexes, grâce à un cadre qui utilise les technologies d’Ingénierie Dirigée par les Modèles (IDM) pour fédérer la simulation, l’analyse formelle et l’émulation. Ceci est rendu possible grâce à la définition d’un langage de spécification unifié de haut niveau, supporté par des capacités de synthèse automatiques d’artéfacts requis par les différentes méthodes d’analyse. En fait, ce travail de thèse propose quatre contributions majeures, qui sont : i) un cadre opérationnel qui utilise l’Architecture Dirigée par les Modèles (ADM) pour supporter ce formalisme de haut niveau, ii) l’intégration de concepts d’horizons multiples pour créer un métamodèle commun qui unifie la simulation, l’analyse formelle et l’émulation, et qui définit la syntaxe abstraite de ce formalisme, iii) des règles de transformation pour la synthèse automatique d’artéfacts à destination de la simulation, de l’analyse formelle et de l’émulation, à partir de tout modèle de système accompagné d’un modèle de ses exigences, et iv) un domaine sémantique pour l’émulation des systèmes à évènements discrets. Tout au long de la thèse, un cas d’école de distribution automatique de boisson est utilisé comme exemple.

Membres du jury :

Jean-Pierre Müller - CIRAD Montpellier
Grégory Zacharewicz - Université de Bordeaux
Mamadou Kaba Traoré (Directeur de thèse) - UCA
David Hill (President du Jury) - UCA
Henri Pierreval - UCA
Andreas Tolk - MITRE Corporation, USA.