TCS / Research / Publications / Testing LTL Formula Translation into B\"uchi Automata
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Testing LTL Formula Translation into Büchi Automata


Heikki Tauriainen and Keijo Heljanko. Testing LTL formula translation into Büchi automata. STTT - International Journal on Software Tools for Technology Transfer, 4(1):57–70, 2002.


Model checkers are often used to verify critical systems, and thus a lot of effort should be put on ensuring their reliability. We describe techniques for testing linear temporal logic (LTL) model checker implementations, focusing especially on LTL-to-Büchi automata translation. We propose a randomized testing approach based on the cross-comparison of independent translator implementations, and present methods for test failure analysis. We give experimental results using an automated tool implementing the testing methodology. This method has helped to detect errors in model checking tools such as Spin. We also propose extending LTL model checkers with a simple counterexample validation algorithm.


verification, model checking, temporal logic, software testing

Suggested BibTeX entry:

    author = {Heikki Tauriainen and Keijo Heljanko},
    journal = {{STTT} - {I}nternational Journal on Software Tools for Technology Transfer},
    number = {1},
    pages = {57--70},
    publisher = {Springer-Verlag},
    title = {Testing {LTL} Formula Translation into {B{\"u}chi} Automata},
    volume = {4},
    year = {2002},

See ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.