Skip to Main content Skip to Navigation
Conference papers

Abstract Animator for Temporal Specifications

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
Abstract : Temporal specifications provide an abstract and powerful framework for modelling (reactive) systems with respect to safety, liveness and fairness properties, for example, telecommunications services and the feature interaction problem. However, techniques and tools are required for analysing temporal specifications as for instance model checking-based techniques or theorem proving-based techniques, because temporal notations are powerful expression of rich concepts (fairness) and are then very difficult to validate. We focus our work on TLA/TLA+ as a specification language, but we require the possibility to validate temporal specifications by animation with respect to an abstraction.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:40:17 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098918, version 1



Dominique Cansell, Dominique Méry. Abstract Animator for Temporal Specifications. Workshop on Modelling & Verification, Françoise Bellegarde, Olga Kouchnarenko & Jacques Julliand, 1999, Besançon, France. ⟨inria-00098918⟩



Record views