Testing Spin’s LTL formula conversion into Büchi automata with randomly generated input

3Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free