Validation of formal specifications

Dominique Méry (1) , Yassine Mokhtari (1)

1 MODEL - MODEL (Méthodes formelles et applications)

TLA, (the Temporal Logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. The purpose of this paper is to develop an animator and a model checker, both based on a subset of TLA, and illustrates how we can combine these tools to validate TLA specifications.

Mots clés: model checker; TLA; validation; animator; animateur; verificateur de modeles

Domaines: Autre [cs.OH]

Dominique Méry, Yassine Mokhtari. Validation of formal specifications. AAAI'99, Fall Symposium, Nov 1999, none, 5 p. ⟨inria-00108115⟩