Skip to Main content Skip to Navigation
Conference papers

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 : Friday, September 4, 2020 - 11:20:23 AM
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