Abstract animator for temporal specifications Application to TLA
Résumé
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.