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

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

Identifiers

  • HAL Id : inria-00098953, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

132