Testing SPIN's LTL formula conversion into Büchi automata with randomly generated input

Reference:

Heikki Tauriainen and Keijo Heljanko. Testing SPIN's LTL formula conversion into Büchi automata with randomly generated input. In Klaus Havelund, John Penix, and Willem Visser, editors, Proceedings of the 7th International SPIN Workshop on Model Checking of Software (SPIN'2000), volume 1885 of Lecture Notes in Computer Science, pages 54–72, Stanford University, California, USA, August 2000. Springer-Verlag.

Abstract:

The use of model checking tools in the verification of reactive systems has become into widespread use. Because the model checkers are often used to verify critical systems, a lot of effort should be put on ensuring the reliability of their implementation. We describe techniques which can be used to test and improve the reliability of linear temporal logic (LTL) model checker implementations based on the automata-theoretic approach. More specifically, we will concentrate on the LTL-to-Büchi automata conversion algorithm implementations, and propose using a random testing approach to improve their robustness. As a case study, we apply the methodology to the testing of this part of the SPIN model checker. We also propose adding a simple counterexample validation algorithm to LTL model checkers to double check the counterexamples generated by the main LTL model checking algorithm.

Keywords:

LTL, Büchi automata

Suggested BibTeX entry:

@inproceedings{TauHel:SPIN2000,
    address = {Stanford University, California, USA},
    author = {Heikki Tauriainen and Keijo Heljanko},
    booktitle = {Proceedings of the 7th International {SPIN} Workshop on Model Checking of Software ({SPIN}'2000)},
    editor = {Klaus Havelund and John Penix and Willem Visser},
    month = {August},
    pages = {54--72},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Testing {SPIN}'s {LTL} formula conversion into {B\"uchi} automata with randomly generated input},
    volume = {1885},
    year = {2000},
}