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.
Type de document :
Communication dans un congrès
Françoise Bellegarde & Olga Kouchnarenko. Workshop on Modelling & Verification, 1999, Besançon, France, 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00098918
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:40:17
Dernière modification le : jeudi 11 janvier 2018 - 06:21:04

Identifiants

  • HAL Id : inria-00098918, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

64