Interprétation de spécifications temporelles à l'aide d'un outil de preuve

Dominique Cansell 1 Dominique Méry 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : La construction d'une spécification TLA+ à partir d'un cahier des charges est une tâche qui peut être facilitée par l'emploi d'outil d'aide à la compréhension dont l'objectif est d'interpréter la spécification formelle et de soumettre des scénarios à l'auteur du cahier des charges. A l'aide d'une étude de cas simple, nous montrons comment un outil de preuve peut être utilisé comme un interprète abstrait pour une spécification temporelle et valider la spécification formelle obtenue par cette technique. Une conséquence de notre étude est de montrer que l'outil Logic-Solver de l'Atelier B est un outil puissant et général qui peut être étendu à l'étude de spécifications temporelles.
Type de document :
Communication dans un congrès
AFADl'98, 1998, none, 13 p, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098541
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:13
Dernière modification le : mardi 24 avril 2018 - 13:34:44

Identifiants

  • HAL Id : inria-00098541, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Interprétation de spécifications temporelles à l'aide d'un outil de preuve. AFADl'98, 1998, none, 13 p, 1998. 〈inria-00098541〉

Partager

Métriques

Consultations de la notice

85