Vérification des Systèmes Réactifs Dans le Modèle Synchrone
Identifieur interne : 00A416 ( Main/Exploration ); 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.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 002687
- to stream Crin, to step Curation: 002687
- to stream Crin, to step Checkpoint: 001C83
- to stream Main, to step Merge: 00AA84
- to stream Main, to step Curation: 00A416
Le 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>
<idno type="wicri:Area/Main/Exploration">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>
<affiliations><list></list>
<tree><noCountry><name sortKey="Azaiez, Ramzi" sort="Azaiez, Ramzi" uniqKey="Azaiez R" first="Ramzi" last="Azaiez">Ramzi Azaiez</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 00A416 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/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= Exploration |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. |