Abstract FR:

La structuration en vues est abondamment utilisee dans les methodes de specifications graphiques pour decrire separement les differents aspects d'un systeme (le controle, les donnees, l'architecture reseau, etc). La possibilite d'assurer la coherence globale d'une modelisation est une question cle pour l'essor de ces methodes. Dans cette these, nous formalisons les notions de vues et de coherence de vues. L'objectif est d'automatiser la verification de proprietes de coherence. Nous proposons un formalisme graphique inspire de la notation uml qui permet de decrire un systeme par une collection de vues traitant chacune d'un aspect du systeme. Les vues sont decrites formellement par des graphes avec multiplicites sur les arcs. Un algorithme permet de verifier la coherence des multiplicites. Afin d'exprimer des criteres de coherence (intra et inter-vues) plus precis, nous introduisons une logique basee sur les predicats arc et chemin. Une procedure de decision complete permet de s'assurer qu'une collection de vues satisfait les contraintes structurelles exprimees dans cette logique. Les aspects dynamiques du systeme sont traduits sous forme de regles de reecriture de graphe et la coherence entre aspects statiques et dynamiques peut egalement etre verifiee automatiquement. Notre formalisme permet d'integrer les notations standards, mais aussi de definir de nouvelles vues et de leur associer des criteres de coherence sans que les concepteurs aient a definir completement la semantique des vues. Nous illustrons notre formalisme sur deux etudes de cas : la conception d'un systeme de gestion de trafic ferroviaire et la modelisation des aspects statiques et dynamiques d'un systeme de controle d'acces. Nous proposons six types de vues