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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00098541
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:03:13 PM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM

Identifiers

  • 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. ⟨inria-00098541⟩

Share

Metrics

Record views

94