Next: , Previous: Copying, Up: Top

1 Overview

lbtt is a tool for testing programs that translate formulas expressed in propositional linear temporal logic (LTL) into Büchi automata. These finite-state automata over infinite words are used e.g. in automata-theoretic model checking [VW86], [Var96], where they can help in detecting errors in the specifications of finite-state hardware or software systems. Usually the model checking procedure involves first composing an automaton with a formal model of a given system, and the result of the composition reveals whether any computation path of the system violates some property that the automaton represents. (For an introduction to model checking techniques in general, see, for example, [CGP99].)

The property to be model checked can be specified as an LTL formula, and the Büchi automaton used for model checking is obtained automatically from the formula with a translation algorithm. (For descriptions and optimization techniques for such algorithms, see the references, for example, [VW86], [Isl94], [GPVW95], [Cou99] [DGV99], [Ete99], [SB00], [EH00], [EWS01], [GO01], [Gei01], [Sch01], [Wol01], [Ete02], [GL02], [GSB02], [Thi02], [Fri03], [GO03], [Lat03], [ST03].) In practice, ensuring the correctness of the implementation of such a translation algorithm is crucial to guarantee the soundness of the implementation of a model checking procedure.

The goal of lbtt is to assist implementing LTL-to-Büchi translation algorithms correctly by providing an automated testing environment for LTL-to-Büchi translators. Testing consists of running LTL-to-Büchi translators on randomly generated (or user-specified) LTL formulas as input and then performing simple consistency checks on the resulting automata to test whether the translators seem to function correctly in practice. (See [TH02] for more information on the theory behind the testing methods.) If the test results suggest that there is an error in an implementation, lbtt can generate sample data which causes a test failure and which may also be useful for debugging the implementation.

Additionally, the testing environment can be used for very basic profiling of different LTL-to-Büchi translators to evaluate their performance.

Note: although lbtt might be able to detect inconsistent behavior in an LTL-to-Büchi translator, it is only a testing tool and is therefore incapable of formally proving any translation algorithm implementation to be correct. Therefore, the test results should never be used as the sole basis for any formal conclusions about the correctness of an implementation.