Vérification des Systèmes Réactifs Dans le Modèle Synchrone
Identifieur interne : 00A416 ( Main/Curation ); précédent : 00A415; suivant : 00A417Vérification des Systèmes Réactifs Dans le Modèle Synchrone
Auteurs : Ramzi AzaiezSource :
English descriptors
- KwdEn :
Abstract
Notre travail s'inscrit dans le cadre de la verification, basee sur une approche deductive, des systemes reactifs decrits a l'aide du langage synchrone LUSTRE. Partant d'une description executable, on genere une representation du systeme dans le langage de specification de SPIKE. Le passage entre les deux formalismes tient compte des specificites des systemes consideres et se fait dans l'objectif d'aboutir a une methode de verification completement automatique de systemes utilisant des variables a valeurs infinies.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002687
- to stream Crin, to step Curation: Pour aller vers cette notice dans l'étape Curation :002687
- to stream Crin, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :001C83
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00AA84
Links to Exploration step
CRIN:azaiez99aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-32">Vérification des Systèmes Réactifs Dans le Modèle Synchrone</title></titleStmt><publicationStmt><idno type="RBID">CRIN:azaiez99a</idno><date when="1999" year="1999">1999</date><idno type="wicri:Area/Crin/Corpus">002687</idno><idno type="wicri:Area/Crin/Curation">002687</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002687</idno><idno type="wicri:Area/Crin/Checkpoint">001C83</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001C83</idno><idno type="wicri:Area/Main/Merge">00AA84</idno><idno type="wicri:Area/Main/Curation">00A416</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Vérification des Systèmes Réactifs Dans le Modèle Synchrone</title><author><name sortKey="Azaiez, Ramzi" sort="Azaiez, Ramzi" uniqKey="Azaiez R" first="Ramzi" last="Azaiez">Ramzi Azaiez</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automatic verification</term><term>lustre</term><term>reactive systems</term><term>spike</term><term>theorem-proving</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-439">Notre travail s'inscrit dans le cadre de la verification, basee sur une approche deductive, des systemes reactifs decrits a l'aide du langage synchrone LUSTRE. Partant d'une description executable, on genere une representation du systeme dans le langage de specification de SPIKE. Le passage entre les deux formalismes tient compte des specificites des systemes consideres et se fait dans l'objectif d'aboutir a une methode de verification completement automatique de systemes utilisant des variables a valeurs infinies.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A416 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 00A416 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Curation
|type= RBID
|clé= CRIN:azaiez99a
|texte= Vérification des Systèmes Réactifs Dans le Modèle Synchrone
}}
| This area was generated with Dilib version V0.6.33. |  |