Browsing by Author "Inggs, Cornelia Petronella"

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    An LTL verification system based on automata theory
    (Stellenbosch : Stellenbosch University, 1999-12) Inggs, Cornelia Petronella; Van Wyk, Cornelia; De Villiers, P. J. A.; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences.
    ENGLISH ABSTRACT: A tool for the design and verification of reactive systems has been developed at the University of Stellenbosch. On-the-fly model checking is used to check correctness properties expressed in CTL (Computation Tree Logic). The system to be verified is modelled in a specification language called ESML. This thesis describes the implementation of an LTL (Linear Time Logic) model checker for ESML. The new model checker is based on automata theory, but uses the same state generator as the CTL model checker. The approach taken is to translate LTL formulas to Buchi automata before the model checking procedure. Verification proceeds by checking the emptiness of 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 generation strategy used in the model checker, and the algorithm to compute the product of the state graph and Buchi automaton are given. Evaluation of the new model checker involved testing and comparison against SPIN and the CTL model checker for ESML. Some efficiency issues are discussed.