RÉSUMÉ :

 La structuration en vues est abondamment utilisée dans les méthodes
 de spécifications graphiques pour décrire séparément les différents
 aspects d'un système (le contrôle, les données, l'architecture
 réseau, etc). La possibilité d'assurer la cohérence globale d'une
 modélisation est une question clé pour l'essor de ces méthodes. Dans
 cette thèse, nous formalisons les notions de vues et de cohérence de
 vues. L'objectif est d'automatiser la vérification de propriétés de
 cohérence.

 Nous proposons un formalisme graphique inspiré de la notation UML qui
 permet de décrire un système par une collection de vues traitant
 chacune d'un aspect du système. Les vues sont décrites formellement
 par des graphes avec multiplicités sur les arcs. Un algorithme permet
 de vérifier la cohérence des multiplicités. Afin d'exprimer des
 critères de cohérence (intra et inter-vues) plus précis, nous
 introduisons une logique basée sur les prédicats «arc» et «chemin».
 Une procédure de décision complète permet de s'assurer qu'une
 collection de vues satisfait les contraintes structurelles exprimées
 dans cette logique. Les aspects dynamiques du système sont traduits
 sous forme de règles de réécriture de graphe et la cohérence entre
 aspects statiques et dynamiques peut également être vérifiée
 automatiquement. Notre formalisme permet d'intégrer les notations
 standards, mais aussi de définir de nouvelles vues et de leur
 associer des critères de cohérence sans que les concepteurs aient à
 définir complètement la sémantique des vues.

 Nous illustrons notre formalisme sur deux études de cas : la
 conception d'un système de gestion de trafic ferroviaire et la
 modélisation des aspects statiques et dynamiques d'un système de
 contrôle d'accès. Nous proposons six types de vues : vue flot de
 données, vue flot de contrôle, vue réseau, vue donnée, vue
 interaction et vue comportement. Ces deux expériences ont démontré
 que nos algorithmes de vérification de cohérence sont utiles pour
 détecter des erreurs de conception.


 MOTS-CLÉS :

   vues multiples, modélisation, spécification, cohérence, diagrammes
   UML, réécriture de graphes, contraintes logiques, vérification,
   architectures logicielles.



 ABSTRACT:

 View structuring is used widely in graphical specification to
 describe separately the various aspects of a system (control flow,
 data flow, communication network, etc). The ability to ensure
 consistency of different views of a system is an important factor for
 the success of design methods that support multiple views. This
 dissertation presents a formalisation of the notion of views and view
 consistency. Our main contribution is the development of consistency
 verification mechanisms.

 We propose a framework inspired by \UML diagrams to describe a system
 as a collection of views ; each view deals with one aspect of the
 system. We provide a formal definition of views described as graphs
 with multiplicities, together with an algorithm to check the
 consistency of multiplicities. We also put forward a simple logic
 based on predicates ``edge'' and ``path'' to express more precise
 (intra and inter-views) consistency requirements. A complete decision
 procedure permits to decide whether a diagram satisfies a given
 structural constraint expressed in this logic. Dynamic aspects of the
 system are translated into graph rewriting rules and consistency
 between static and dynamic aspects can be automatically checked. Our
 proposal fulfills the requirements of designers: first, standard
 notations can be integrated in our framework. Second, it is possible
 to define new views and to provide them with consistency criteria
 expressed in our logic. Thus, consistency checking can be done
 without defining the complete semantics of each view.

 Our framework is illustrated with two case studies: a design of a
 train control system and a model of static and dynamic aspects of an
 access control system. We propose six kinds of views describing
 several aspects of the systems: the data flow, control flow, network,
 data, interaction and behaviour views. These two experiments
 demonstrate that our three verification algorithms are useful in
 detecting design problems.


 KEYWORDS:
 
   multiples views, system modeling, specification, consistency, UML
   diagrams, graph rewriting, logic constraints, verification,
   software architecture.