L'objectif de cette thèse est de donner une méthode de spécification pour des réseaux de processus communicants. Les processus sont spécifiés indépendamment les uns des autres et sont liés par la suite à l'aide de canaux de communication. Un processus est caractérisé par un ensemble d'objets qui lui sont associés, et par un ensemble d'opérations créant ces objets, ou les modifiant. Le cadre de travail que nous avons choisi pour définir objets et opérations, est la théorie des types abstraits algébriques. Les comportements possibles du processus sont donnés par une formule de logique temporelle (SOTL), où l'atome de base est l'action. Les actions d'un processus sont l'affectation (éventuellement gardée) et le test, et sont construites à partir des opérations pré-citées. Nous prenons comme générateur de modèles de la formule de logique temporelle, un automate de Büchi. Ainsi tout comportement du processus est un chemin infini dans l'automate. Nous développons également une seconde logique temporelle du premier ordre (POTL) permettant de décrire des propriétés d'invariance ou de fatalité sur les comportements des processus. Les propriétés que nous donnons sont essentiellement des relations sur les histoires des canaux. Connaissant l'automate associé à la spécification temporelle du processus, on veut vérifier une assertion POTL à partir de l'automate. Vérifier une assertion temporelle sur un automate consiste à éliminer les opérateurs temporels en progressant dans les chemins de l'automate. Par exemple, vérifier \bigcirc \phi en le nœud s de l'automate consiste à prouver \phi en tous les successeurs directs de s, l'opérateur \bigcirc se trouvant ainsi éliminé. D'autre règles sont données pour éliminer les \Box et \diamond. Une preuve temporelle se ramène donc finalement à un arbre de preuves élémentaires. Nous donnons enfin la correction de la méthode. Les canaux sont également spécifiés de manière algébrique. Nous associons à tout canal un type abstrait qui en fait donne sa politique de communication. Deux macros (suite d'actions) lui sont associées : Produire et Consommer. Ainsi lors de la mise en parallèle, il suffira de lier ces macros aux macros provisoires utilisées lors de la spécification des processus. Nous donnons un langage succinct permettant de construire un réseau à partir de spécifications de processus et de spécifications de canaux. L'automate associé au réseau sera l'automate associé à la conjonction des différentes spécifications auquelles on ajoutera éventuellement une contrainte. Le chapitre 1 est une introduction générale au contenu de la thèse. Le chapitre 2 traite de la logique temporelle et des automates d'état finis sur mots infinis. Le chapitre 3 examine quelques travaux relatifs aux spécifications et preuves de processus communicants. le chapitre 4 décrit notre cadre de travail (logique SOTL et POTL) et donne quelques exemples de spécifications. Le chapitre 5 donne notre système de preuve et sa correction. Le chapitre 6 aborde le problème de communication et de la formation de réseaux de processus. Le chapitre 7 traite de la construction de processus par raffinements successifs. Vient en dernier lieu la conclusion.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D841 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D841 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     CRIN:carrez91a
   |texte=   Spécification, vérification et raffinement de réseaux de processus communicants
}}