Automated Testing of Büchi Automata Translators for Linear Temporal Logic

Reference:

Heikki Tauriainen. Automated testing of Büchi automata translators for linear temporal logic. Research Report A66, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2000.

Abstract:

The formal verification of finite-state reactive and concurrent systems against temporal logical requirements can be done by model checking, which has the advantage of being well suited for automation. However, reasoning about the correctness of systems using automated techniques places high demands for ensuring the reliability of the model checking tools themselves.

This work describes testing methods for detecting implementation errors in a specific class of algorithms required in the automata-theoretic model checking procedure for propositional linear temporal logic (LTL). These algorithms are used for translating temporal requirements into Büchi automata, which are used in the model checking process. Most of the test methods can be easily integrated into an automatic testing tool for translation algorithm implementations. Experimental results using a randomized tool for testing the correctness of several implementations included in real model checkers are presented. This testing has proved to be an effective method for finding implementation errors in the translators.

This work also presents a restricted LTL model checking algorithm designed to work in a very simple subclass of systems, on which the analysis of test failures is based. This algorithm can be used to automatically confirm the incorrectness of a translation algorithm implementation.

Keywords:

Model checking, linear temporal logic, Büchi automata, algorithm testing

Suggested BibTeX entry:

@techreport{HUT-TCS-A66,
    address = {Espoo, Finland},
    author = {Heikki Tauriainen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A66},
    pages = {86},
    title = {Automated Testing of {B}\"uchi Automata Translators for Linear Temporal Logic},
    type = {Research Report},
    year = {2000},
}