Animating TLA Specifications

Yassine Mokhtari 1 Stephan Merz
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : TLA (the Temporal Logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, with the intent to facilitate the communication between domain and solution experts in the design of reactive systems.
Type de document :
Communication dans un congrès
H. Ganzinger, D. McAllester, A. Voronkov. International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, Springer, 1705, pp.92--110, 1999, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées

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

Identifiants

  • HAL Id : inria-00099016, version 1

Collections

Citation

Yassine Mokhtari, Stephan Merz. Animating TLA Specifications. H. Ganzinger, D. McAllester, A. Voronkov. International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, Springer, 1705, pp.92--110, 1999, Lecture Notes in Artificial Intelligence. 〈inria-00099016〉

Partager

Métriques

Consultations de la notice

112