An LTL verification system based on automata theory

Inggs, Cornelia Petronella ; Van Wyk, Cornelia (1999-12)

Dissertion (M.Sc.) -- University of Stellenbosch, 1999.

Thesis

ENGLISH ABSTRACT: A tool for the design and verification ofreactive 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 Biichi automata before the model checking procedure. Verification proceeds by checking the emptiness of the product of the Biichi automaton and state graph generated from the ESML model. The algorithms needed to build the Biichi 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 Biichi 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.

AFRIKAANSE OPSOMMING: 'n Stelsel vir die ontwerp en verifikasie van reaktiewe stelstels is by die Universiteit van Stellenbosch ontwikkel. Modeltoetsing word gebruik om korrektheidseienskappe, uitgedruk in CTL ('n vertakkende temp orale logika), te toets. Die stelsel wat verifieer moet word, word modelleer in die hoevlak spesifikasietaal ESML. Die tesis beskryf die implementering van 'n LTL (lineere tyd logika) modeltoetser vir ESML. Die nuwe modeltoetser is gebaseer op outomaatteorie, maar gebruik dieselfde toestandgenerasie tegniek vir ESML as die CTL modeltoetser. Die benadering wat gevolg is, is om LTL for mules om te skakel in Biichi outomate voor die modeltoetsprosedure. Verifiering geskied dan deur te toets of die produk van die Biichi outomaat en toestanddiagram van die ESML modelleeg is. Die algoritmes om Biichi outomate vanaf LTL formules te bou, die toestandgenerasie tegniek van die modeltoetser, en die algoritme om die prod uk van 'n Biichi outomaat en toestanddiagram te bereken, word gegee. Evaluasie van die nuwe modeltoetser het toetsing en vergelykings met SPIN en die CTL modeltoetser ingesluit. 'n Aantal effektiwiteitskwessies word bespreek.

Please refer to this item in SUNScholar by using the following persistent URL: http://hdl.handle.net/10019.1/51128
This item appears in the following collections: