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 metadatas

https://hal.inria.fr/inria-00098918
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:40:17 AM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM

Identifiers

  • HAL Id : inria-00098918, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

81