Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication
Identifieur interne : 001E81 ( Crin/Corpus ); précédent : 001E80; suivant : 001E82Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication
Auteurs : Joël Toussaint ; Luis VegaSource :
English descriptors
- KwdEn :
Abstract
Nous présentons dans cet article les formalismes utilisés pour exprimer puis pour vérifier des propriétés temporelles sur la communication. Nous montrons comment passer d'un modèle adapté à l'expression de ces propriétés à un modèle décrivant le comportement de l'application et supportant la vérification. Cette modélisation est appliquée au comportement observable entre une couche demandant des services soumis à des contraintes et une couche utilisant ces services avec des performances données. L'expression des contraintes et des caractéristiques est spécifiée sur des séquences temporisées d'événements. Puis les techniques de vérification de propriétés exploitant les réseaux de Petri temporels sont présentées. Les liens entre les modèles sont explicités à chaque fois.
Links to Exploration step
CRIN:toussaint97bLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-40">Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication</title></titleStmt><publicationStmt><idno type="RBID">CRIN:toussaint97b</idno><date when="1997" year="1997">1997</date><idno type="wicri:Area/Crin/Corpus">001E81</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication</title><author><name sortKey="Toussaint, Joel" sort="Toussaint, Joel" uniqKey="Toussaint J" first="Joël" last="Toussaint">Joël Toussaint</name></author><author><name sortKey="Vega, Luis" sort="Vega, Luis" uniqKey="Vega L" first="Luis" last="Vega">Luis Vega</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>communication</term><term>time Petri net</term><term>time constraints</term><term>validation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-2813">Nous présentons dans cet article les formalismes utilisés pour exprimer puis pour vérifier des propriétés temporelles sur la communication. Nous montrons comment passer d'un modèle adapté à l'expression de ces propriétés à un modèle décrivant le comportement de l'application et supportant la vérification. Cette modélisation est appliquée au comportement observable entre une couche demandant des services soumis à des contraintes et une couche utilisant ces services avec des performances données. L'expression des contraintes et des caractéristiques est spécifiée sur des séquences temporisées d'événements. Puis les techniques de vérification de propriétés exploitant les réseaux de Petri temporels sont présentées. Les liens entre les modèles sont explicités à chaque fois.</div></front></TEI><BibTex type="inproceedings"><ref>toussaint97b</ref><crinnumber>97-R-058</crinnumber><category>3</category><equipe>TRIO</equipe><author><e>Toussaint, Joël</e><e>Vega, Luis</e></author><title>Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication</title><booktitle>{Renpar'9 - Rencontres francophones du Parallélisme, Lausanne, Suisse}</booktitle><year>1997</year><pages>67-70</pages><month>may</month><url>http://www.loria.fr/publications/1997/97-R-058/97-R-058.ps</url><keywords><e>communication</e><e>time constraints</e><e>validation</e><e>time Petri net</e></keywords><abstract>Nous présentons dans cet article les formalismes utilisés pour exprimer puis pour vérifier des propriétés temporelles sur la communication. Nous montrons comment passer d'un modèle adapté à l'expression de ces propriétés à un modèle décrivant le comportement de l'application et supportant la vérification. Cette modélisation est appliquée au comportement observable entre une couche demandant des services soumis à des contraintes et une couche utilisant ces services avec des performances données. L'expression des contraintes et des caractéristiques est spécifiée sur des séquences temporisées d'événements. Puis les techniques de vérification de propriétés exploitant les réseaux de Petri temporels sont présentées. Les liens entre les modèles sont explicités à chaque fois.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001E81 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001E81 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:toussaint97b
|texte= Modèles pour l'Expression et la Vérification de Propriétés Temporelles dans la Communication
}}
| This area was generated with Dilib version V0.6.33. |  |