An LTL verification system based on automata theory

[摘要] ENGLISH ABSTRACT: A tool for the design and verification of reactive systems has been developed at the Universityof Stellenbosch. On-the-fly model checking is used to check correctness properties expressedin CTL (Computation Tree Logic). The system to be verified is modelled in a specificationlanguage called ESML.This thesis describes the implementation of an LTL (Linear Time Logic) model checker forESML. The new model checker is based on automata theory, but uses the same state generatoras the CTL model checker. The approach taken is to translate LTL formulas to Buchi automatabefore the model checking procedure. Verification proceeds by checking the emptinessof the product of the Buchi automaton and state graph generated from the ESML model.The algorithms needed to build the Buchi automaton from an LTL formula, the state generationstrategy used in the model checker, and the algorithm to compute the product of thestate graph and Buchi automaton are given. Evaluation of the new model checker involvedtesting and comparison against SPIN and the CTL model checker for ESML. Some efficiencyissues are discussed.

[发布机构] Stellenbosch University