Automated Testing of Buechi Automata Translators for Linear Temporal Logic.

摘要

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 translate temporal requirements into Buechi automata that 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 helps to automatically confirm the incorrectness of a translation algorithm implementation.