Vérification formelle de propriétés temporelles d'une application distribuée temps réel
Identifieur interne : 001E80 ( Crin/Corpus ); précédent : 001E79; suivant : 001E81Vérification formelle de propriétés temporelles d'une application distribuée temps réel
Auteurs : Joël Toussaint ; Françoise Simonot-LionSource :
English descriptors
Abstract
Les travaux présentés dans ce papier apportent un élément de solution pour la validation d'applications temps réel distribuées en proposant une méthode de vérification formelle de propriétés spécifiques. Plus précisément, nous montrons comment analyser le modèle, exprimé suivant le formalisme des réseaux de Petri temporels, d'une telle application en intégrant les aspects fonctionnels (fonctions, liens de données et de contrôle) et l'architecture informatique support. Le travail repose sur l'exploitation du graphe de classes déduit du réseau de Petri temporel pour vérifier que des contraintes de temps exprimées sur des dates d'occurrences d'événements seront respectées par une implantation et une distribution. Les méthodes d'analyse pour certains types de contraintes font l'objet de ce document.
Links to Exploration step
CRIN:toussaint97aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-339">Vérification formelle de propriétés temporelles d'une application distribuée temps réel</title></titleStmt><publicationStmt><idno type="RBID">CRIN:toussaint97a</idno><date when="1997" year="1997">1997</date><idno type="wicri:Area/Crin/Corpus">001E80</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Vérification formelle de propriétés temporelles d'une application distribuée temps réel</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="Simonot Lion, Francoise" sort="Simonot Lion, Francoise" uniqKey="Simonot Lion F" first="Françoise" last="Simonot-Lion">Françoise Simonot-Lion</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>formal verification</term><term>time Petri net</term><term>time contraints</term><term>validation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-2001">Les travaux présentés dans ce papier apportent un élément de solution pour la validation d'applications temps réel distribuées en proposant une méthode de vérification formelle de propriétés spécifiques. Plus précisément, nous montrons comment analyser le modèle, exprimé suivant le formalisme des réseaux de Petri temporels, d'une telle application en intégrant les aspects fonctionnels (fonctions, liens de données et de contrôle) et l'architecture informatique support. Le travail repose sur l'exploitation du graphe de classes déduit du réseau de Petri temporel pour vérifier que des contraintes de temps exprimées sur des dates d'occurrences d'événements seront respectées par une implantation et une distribution. Les méthodes d'analyse pour certains types de contraintes font l'objet de ce document.</div></front></TEI><BibTex type="inproceedings"><ref>toussaint97a</ref><crinnumber>97-R-006</crinnumber><category>3</category><equipe>TRIO</equipe><author><e>Toussaint, Joël</e><e>Simonot-Lion, Françoise</e></author><title>Vérification formelle de propriétés temporelles d'une application distribuée temps réel</title><booktitle>{Real-Time Systems - RTS'97}</booktitle><year>1997</year><series>Teknea</series><pages>53-66</pages><keywords><e>validation</e><e>formal verification</e><e>time Petri net</e><e>time contraints</e></keywords><abstract>Les travaux présentés dans ce papier apportent un élément de solution pour la validation d'applications temps réel distribuées en proposant une méthode de vérification formelle de propriétés spécifiques. Plus précisément, nous montrons comment analyser le modèle, exprimé suivant le formalisme des réseaux de Petri temporels, d'une telle application en intégrant les aspects fonctionnels (fonctions, liens de données et de contrôle) et l'architecture informatique support. Le travail repose sur l'exploitation du graphe de classes déduit du réseau de Petri temporel pour vérifier que des contraintes de temps exprimées sur des dates d'occurrences d'événements seront respectées par une implantation et une distribution. Les méthodes d'analyse pour certains types de contraintes font l'objet de ce document.</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 001E80 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001E80 | 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:toussaint97a
|texte= Vérification formelle de propriétés temporelles d'une application distribuée temps réel
}}
| This area was generated with Dilib version V0.6.33. |  |