Abstract animator for temporal specifications Application to TLA

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 : In this paper, we explain how we use abstract interpretation for analysing temporal specifications in TLA. An analysis is obtained by building a predicate behavior which checks the specification. Abstract interpretation allows us to transit from a concrete world to an abstract world (generally finite). Using abstract interpretation, we build abstract predicate behaviors and, in general, if the abstract interpretation is sufficiently powerful and expressive, we can build a finite graph of abstract predicates to analyse a temporal specification. TLA/TLA is based on an untyped framework, namely the ZF set theory and we show how abstract interpretation fits the requirements of untyping and makes easier the analysis of temporal specifications.
Type de document :
Communication dans un congrès
Agostino Cortesi and Gilberto Fil. International Symposium on Static Analysis - SAS'99, 1999, Venise, Italie, Springer Verlag, 1694, pp.284-299, 1999, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098953
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:40:47
Dernière modification le : mardi 24 avril 2018 - 13:34:55

Identifiants

  • HAL Id : inria-00098953, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Abstract animator for temporal specifications Application to TLA. Agostino Cortesi and Gilberto Fil. International Symposium on Static Analysis - SAS'99, 1999, Venise, Italie, Springer Verlag, 1694, pp.284-299, 1999, Lecture Notes in Computer Science. 〈inria-00098953〉

Partager

Métriques

Consultations de la notice

107