XTL: A Meta-Language and Tool for Temporal Logic Model-Checking

Radu Mateescu and Hubert Garavel

Proceedings of the International Workshop on Software Tools for Technology Transfer STTT'98 (Aalborg, Denmark), July 1998.

Abstract:

We present a temporal logic model-checking environment based on a new language called XTL (eXecutable Temporal Language). XTL is a functional programming language designed to allow a compact description of various temporal logic operators, which are evaluated over a Labelled Transition System (LTS). XTL offers primitives to access the data values (possibly) contained in the states and labels of the LTS, as well as to explore the transition relation. The temporal logic operators are implemented by means of iteration expressions computing sets of states and sets of transitions. Various useful modal and temporal logics like HML, CTL, LTAC, and ACTL, have been implemented in XTL, and several industrial case-studies, such as the BRP protocol designed by Philips, the IEEE-1394 serial bus standardized by IEEE, and the CFS protocol developed by Bull and INRIA, have been successfully validated using the XTL model-checker.

10 pages

PDF

PostScript