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.
CITATION STYLE
Tauriainen, H., & Heljanko, K. (2000). Testing Spin’s LTL formula conversion into Büchi automata with randomly generated input. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1885, pp. 54–72). Springer Verlag. https://doi.org/10.1007/10722468_4
Mendeley helps you to discover research relevant for your work.