Validation of formal specifications

Dominique Méry 1 Yassine Mokhtari 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download
Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 3:58:15 PM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM
Long-term archiving on : Wednesday, March 29, 2017 - 1:29:59 PM


  • HAL Id : inria-00108115, version 1



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



Record views


Files downloads