Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:40:47 AM
Last modification on : Friday, September 4, 2020 - 11:20:25 AM


  • HAL Id : inria-00098953, version 1



Dominique Cansell, Dominique Méry. Abstract animator for temporal specifications Application to TLA. International Symposium on Static Analysis - SAS'99, Gilberto Fil & Agostino Cortesi, 1999, Venise, Italie, pp.284-299. ⟨inria-00098953⟩



Record views