HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Cited literature [7 references]  Display  Hide  Download

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 3:58:15 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 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