Dans cette thèse, nous décrivons comment on peut utiliser un diagramme de séquence UML avec des contraintes de temps MARTE pour spécifier complètement le comportement des systèmes à base de composants tout en faisant abstraction des rôles fonctionnels des composants. Nous avons proposé une approche qui permet d'analyser ces spécifications d'une manière modulaire. Pour cela, nous avons attribué une sémantique opérationnelle aux diagrammes de séquence en les traduisant vers les TIOSTS qui sont des automates symbolique et temporisé. Nous avons utilisé des techniques d'exécution symbolique pour calculer les exécutions du système sous la forme d'un arbre symbolique. Nous avons défini des mécanismes de projection pour extraire l'arbre d'exécution associé à un composant sous-jacent. L'arbre résultant de la projection caractérise les comportements attendus du composant et peut être utilisé comme une référence pour valider le système bout par bout. Pour ce faire, nous nous sommes intéressés à des techniques de test. Nous avons présenté un résultat qui ramène la conformité du système à la conformité des composants qui le composent. Sur la base de ces résultats, nous avons proposé une méthodologie incrémentale de test basé sur des spécifications décrites sous la forme de diagrammes de séquence. / In this thesis, we describe how to use UML sequence diagrams with MARTE timing constraints to specify entirely the behavior of component-based systems while abstracting as much as possible the functional roles of components composing it. We have shown how to conduct compositional analysis of such specifications. For this, we have defined operational semantics to sequence diagrams by translating them into TIOSTS which are symbolic automata with timing constraints. We have used symbolic execution techniques to compute possible executions of the system in the form of a symbolic tree. We have defined projection mechanisms to extract the execution tree associated with any distinguished component. The resulting projected tree characterizes the possible behaviors of the component with respect to the context of the whole system specification. As such, it represents a constraint to be satisfied by the component and it can be used as a correctness reference to validate the system in a compositional manner. For that purpose, we have grounded our validation framework on testing techniques. We have presented compositional results relating the correctness of a system to the correctness of components. Based on these results, we have defined an incremental approach for testing from sequence diagrams.

Les MSG (pour « Message Sequence Graphs ») sont un formalisme bien connu et souvent utilisé pour décrire des ensembles de scénarios de manière visuelle dans le domaine des protocoles de communication. Nous nous intéressons dans la première partie de la thèse à la détection de la divergence, la vérification de la coopération globale ainsi que la vérification de propriétés d’accessibilité et de couverture. Notre première contribution consiste à utiliser des solveurs SAT afin de résoudre ces problèmes efficacement. Afin de munir le formalisme des MSG de compteurs, de timers et d’autres aspects, nous introduisons le modèle des PNS (pour « réseaux de Petri avec états ») et une sémantique de processus non-branchants. Ce modèle est non seulement plus expressif que les MSG, mais il permet également des spécifications plus concises. Nous nous intéressons à trois problèmes de vérification classiques sur l’ensemble des marquages accessibles par les préfixes des processus : le caractère borné, la couverture et l’accessibilité. Afin de considérer des systèmes paramétrés, nous introduisons également la notion de borne semi-structurelle. Cela consiste à fixer le marquage initial d’un sous-ensemble approprié de places, puis à vérifier que le système est borné, quelles que soient les valeurs des paramètres. Nous montrons comment un dépliage conduit à un problème plus simple à vérifier. Une caractéristique particulièrement attrayante des MSG et des PNS réside dans leur représentation graphique similaire à un automate. Il est donc intéressant de décrire les bugs de manière visuelle. Nous montrons comment calculer en temps polynomial une représentation simple et concise d’un bug. / Message Sequence Charts (MSCs) are a popular model often used for the docu- mentation of telecommunication protocols. In the first part of the thesis, we focus on detecting process divergence, checking global-cooperation and checking reachability properties. Our first contribution is to use SAT solvers to solve these problems effectively. In order to study MSC specifications with counters, timers and other features, we introduce the model of Petri nets with states together with a non-branching non-sequential process seman- tics. We obtain a framework that is more expressive and more concise than MSGs. We consider then three classical verification problems for the set of markings reached by prefixes of processes : boundedness, covering and reachability. We consider also the notion of semi-structural property in order to study parametrized sys- tems. In this way, only part of the places are provided with an initial marking. Unfolding such a system leads to a simpler problem in the form of a linear programme. A particularly attractive feature of MSG and PNS lies in their graphical representation similar to an automaton. So, it is interesting to describe the bugs visually. We show how to compute in polynomial time a simple and concise representation of a bug.

Nous proposons une approche semi-automatique pour la rétro-ingénierie des diagrammes de séquence d’UML. Notre approche commence par un ensemble de traces d'exécution qui sont automatiquement alignées pour déterminer le comportement commun du système. Les diagrammes de séquence sont ensuite extraits avec l’aide d’une visualisation interactive, qui permet la navigation dans les traces d'exécution et la production des opérations d'extraction. Nous fournissons une illustration concrète de notre approche avec une étude de cas, et nous montrons en particulier que nos diagrammes de séquence générés sont plus significatifs et plus compacts que ceux qui sont obtenus par les méthodes automatisées. / We propose a semi-automated approach for the reverse engineering of UML sequence diagrams. Our approach starts with a set of execution traces that are automatically aligned to determine the common behavior. Sequence diagrams are then extracted with the help of an interactive visualization, which allows navigating though execution traces and performing extraction operations. We provide a concrete illustration of our approach with a case study, and show in particular that the resulting diagrams are more meaningful and more compact than those extracted by automated approaches.

Nous proposons une approche semi-automatique pour la rétro-ingénierie des diagrammes de séquence d’UML. Notre approche commence par un ensemble de traces d'exécution qui sont automatiquement alignées pour déterminer le comportement commun du système. Les diagrammes de séquence sont ensuite extraits avec l’aide d’une visualisation interactive, qui permet la navigation dans les traces d'exécution et la production des opérations d'extraction. Nous fournissons une illustration concrète de notre approche avec une étude de cas, et nous montrons en particulier que nos diagrammes de séquence générés sont plus significatifs et plus compacts que ceux qui sont obtenus par les méthodes automatisées. / We propose a semi-automated approach for the reverse engineering of UML sequence diagrams. Our approach starts with a set of execution traces that are automatically aligned to determine the common behavior. Sequence diagrams are then extracted with the help of an interactive visualization, which allows navigating though execution traces and performing extraction operations. We provide a concrete illustration of our approach with a case study, and show in particular that the resulting diagrams are more meaningful and more compact than those extracted by automated approaches.