Interprétation de spécifications temporelles à l'aide d'un outil de preuve
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.