Preuves de systèmes réactifs dans le modèle synchrone

Julien Musset 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Prouver la correction de programmes informatiques devient une contrainte importante dans la réalisation de logiciels. Les systèmes réactifs se développent comme modèles de gestion de flots de données. Le but de ce travail est de proposer une spécification logique de tels systèmes afin de prouver des propriétés grâce au système de démonstration automatique SPIKE.
Type de document :
Rapport
[Stage] 99-R-300 || musset99a, 1999, 30 p
Liste complète des métadonnées

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

Identifiants

  • HAL Id : inria-00098855, version 1

Collections

Citation

Julien Musset. Preuves de systèmes réactifs dans le modèle synchrone. [Stage] 99-R-300 || musset99a, 1999, 30 p. 〈inria-00098855〉

Partager

Métriques

Consultations de la notice

116