Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

.

Réflexion théorique visant à dégager les principes communs à la très grande majorité des langages de description de systèmes logiques. Presentation de CONLAN. Exposé d'un modèle d'évaluation permettant de spécifier l'interprétation des primitives d'un langage de description de systèmes logiques.

.

Théorèmes de points fixes dans les treillis complets, étude du comportement d'un système dynamique discret, analyse sémantique exacte des programmes et applications. Méthodes constructives d'approximation de points fixes d'opérateurs monotone sur un treillis complet. Analyse sémantique approchée des programmes et applications. Analyse sémantique des procédures recursives.

Nous nous sommes intéressé à la logique équationnelle en tant que support de la vérification des programmes impératifs. Notre approche vise le double objectif d'automatiser la vérification des propriétés de programmes et de proposer un formalisme pour raisonner sur les programmes adapté aux acteurs du développement des logiciels. Précisément, les travaux de cette thèse portent sur la traduction automatique des programmes impératifs vers la logique équationnelle. Nous avons considéré deux classes de programmes. Dans la première, la seule instruction avec effet de bord du langage est l'affectation. Nous présentons l'algorithme de traduction d'un programme en un ensemble d'équations sous la forme d'un système de réécriture définissant la sémantique du langage. Nous montrons la convergence du système de réécriture à l'aide d'un démonstrateur de théorèmes. Pour la seconde classe, nous ajoutons au langage appel par référence et listes mutables. Ces deux mécanismes introduisent la possibilité de manipuler des alias dans les programmes. Nous énonçons des restrictions sur l'utilisation des alias moyennant lesquelles nous proposons un algorithme pour la traduction en équations des programmes de cette seconde classe. La définition équationnelle obtenue ne s'appuie pas sur un modèle de la mémoire. Les équations produites par la traduction d'un programme peuvent alors être utilisées dans des systèmes de preuve afin de vérifier des propriétés du programme, elles-mêmes exprimées par des équations. Nous validons notre approche par une implantation des algorithmes et par la preuve de propriétés de programmes non triviales à l'aide des équations produites par notre méthode.

Le couplage des approches orientées objets avec la méthode B est une piste pour l'amélioration de l'activité de spécification et de développement de logiciels. La méthode B fournit des notations et des outils supports puissants permettant de modéliser et de vérifier des modèles. Les approches objets fournissent des mécanismes intéressants pour la structuration et le développement de gros systèmes. L'apport de notre travail de thèse contribue aux activités de couplage entre ces deux formalismes en utilisant le prouveur de B pour valider et vérifier des spécifications UML.<br /><br />En étendant les schémas de dérivation d'UML vers B proposés dans des travaux précédents réalisés dans l'équipe de recherche Dédale, nous proposons une approche de dérivation en B de méta-modèles UML, de diagrammes statiques et de diagrammes dynamiques. L'objectif de cette proposition est de vérifier la sémantique et la cohérence entre différents diagrammes de spécifications UML.<br /><br />Notre thèse apporte aussi une contribution au développement de spécifications objets en utilisant la méthode B. La première proposition concerne la prise en compte de certains types d'associations entre classes lors de la dérivation en B. La deuxième proposition concerne la validation de spécifications orientées objets décrites à l'aide de diagrammes de séquence UML2.0.

Les systèmes d'édition collaborative permettent à plusieurs utilisateurs d'éditer simultanément un document. Aujourd'hui, l'édition collaborative massive est une réalité. Il ne s'agit plus d'éditer à quelques utilisateurs mais à des milliers d'utilisateurs répartis dans le monde. Les éditeurs collaboratifs actuels n'ont pas été conçus pour supporter un nombre si important d'utilisateurs. Les problèmes soulevés ne sont pas d'ordre technologique, ils remettent en cause les fondements algorithmiques des éditeurs. L'objectif de cette thèse est de proposer des algorithmes adaptés à l'édition collaborative massive. Nous montrons qu'un tel algorithme doit assurer trois critères : convergence des données, préservation des intentions et passage à l'échelle. Au regard de l'état de l'art, seul le modèle des transformées opérationnelles (OT) peut concilier ces trois critères.<br />La première contribution de cette thèse montre que l'approche OT conçue pour des éditeurs temps réel peut être utilisée pour réaliser des outils asynchrones. Nous avons réalisé un gestionnaire de configurations dénommé SO6. La seconde contribution est une approche formelle à la conception et à la vérification de fonctions de transformation pour le modèle OT. Cette approche repose sur un démonstrateur automatique de théorème. Avec cette approche, nous montrons que toutes les fonctions de transformation proposées jusqu'ici sont fausses. La troisième et dernière contribution de ce travail est un nouvel algorithme de réplication optimiste (WOOT) adapté à l'édition collaborative massive de structures linéaires. Ce modèle repose sur le calcul monotone d'une extension linéaire des ordres partiels formés par les relations entre les différents éléments de la structure.

L'augmentation en taille et en complexité des systèmes réactifs font que leur vérification est de plus en plus difficile à comprendre et à appréhender. Dans cette thèse, une approche est proposée pour spécifier et vérifier compositionnellement certains de ces systèmes.<br /><br />Cette approche est basée sur un principe de décomposition supportant un raffinement compositionnel au niveau des composants et au niveau de leur produit synchronisé~: une méthode est présentée pour vérifier le raffinement d'un système à composants à partir du raffinement de ses composants.<br /><br />Les propriétés LTL sont préservées par le raffinement compositionnel présenté ici. De plus, certaines propriétés -- comme les invariants et les propriétés LTL de sûreté -- peuvent être vérifiées compositionnellement durant la phase de vérification du raffinement.<br /><br />Un outil, nommé SynCo, implante cette approche de vérification compositionnelle. Les différents aspects de ce travail sont illustrés par plusieurs exemples~: un robot industriel, un système d'essuyage et un porte-monnaie électronique.

La vérification formelle de systèmes concurrents temps réels se heurte au problème de l'explosion du nombre d'états à explorer. Ce problème connu sous le nom ``d'explosion combinatoire'' à plusieurs causes. Cette thèse s'intéresse à deux d'entre-elles. · Pour lutter contre l'explosion due à la représentation du parallélisme par l'entrelacement d'actions, cette thèse propose des techniques basées sur l'approche des ordres-partiels pour construire un graphe réduit. Pour exploiter les ordres-partiels, les techniques proposées utilisent la construction de « pas de transitions » afin de limiter le nombre d'états explorés. Différentes constructions des « pas de transitions » sont proposées en fonction de la classe de propriétés que l'on souhaite préserver (Blocages, Équivalence de traces, LTL). · Pour lutter contre l'explosion due aux contraintes temporelles, cette thèse propose une approche par sur-approximation du comportement. L'objectif est d'avoir un graphe abstrait du comportement de la sur-approximation plus petit que celui du système. Comme classiquement, les techniques d'abstractions permettent d'obtenir une procédure de décision semi-effective. Lorsque l'analyse de la sur-approximation ne permet pas de conclure, la thèse propose une méthode effective permettant de conclure pour les formules de LTL: le système est analysé, guidé par les résultats obtenus sur la sur-approximation. Cette thèse présente les algorithmes de ces différentes techniques de réduction et l'outil tina (http://www.laas.fr/tina) dans lequel ils ont été implémentés.