Vérification des Systèmes Réactifs Dans le Modèle Synchrone

Ramzi Azaiez 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : 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.
Type de document :
Rapport
[Stage] 99-R-209 || azaiez99a, 1999, 59 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00098836
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:39:02
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098836, version 1

Collections

Citation

Ramzi Azaiez. Vérification des Systèmes Réactifs Dans le Modèle Synchrone. [Stage] 99-R-209 || azaiez99a, 1999, 59 p. 〈inria-00098836〉

Partager

Métriques

Consultations de la notice

61