Spécification, vérification et raffinement de réseaux de processus communicants
Identifieur interne : 00D841 ( Main/Exploration ); précédent : 00D840; suivant : 00D842Spécification, vérification et raffinement de réseaux de processus communicants
Auteurs : F. CarrezSource :
English descriptors
- KwdEn :
Abstract
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.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 000D16
- to stream Crin, to step Curation: 000D16
- to stream Crin, to step Checkpoint: 003918
- to stream Main, to step Merge: 00E119
- to stream Main, to step Curation: 00D841
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="5">Spécification, vérification et raffinement de réseaux de processus communicants</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:carrez91a</idno>
<date when="1991" year="1991">1991</date>
<idno type="wicri:Area/Crin/Corpus">000D16</idno>
<idno type="wicri:Area/Crin/Curation">000D16</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">000D16</idno>
<idno type="wicri:Area/Crin/Checkpoint">003918</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003918</idno>
<idno type="wicri:Area/Main/Merge">00E119</idno>
<idno type="wicri:Area/Main/Curation">00D841</idno>
<idno type="wicri:Area/Main/Exploration">00D841</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Spécification, vérification et raffinement de réseaux de processus communicants</title>
<author><name sortKey="Carrez, F" sort="Carrez, F" uniqKey="Carrez F" first="F." last="Carrez">F. Carrez</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>abstract data types</term>
<term>concurrency</term>
<term>network of communication processes</term>
<term>proof of properties</term>
<term>specification</term>
<term>temporal logics</term>
<term>trace logic</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="fr" wicri:score="-5735">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.</div>
</front>
</TEI>
<affiliations><list></list>
<tree><noCountry><name sortKey="Carrez, F" sort="Carrez, F" uniqKey="Carrez F" first="F." last="Carrez">F. Carrez</name>
</noCountry>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D841 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D841 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{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 }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |