An LTL verification system based on automata theory
Date
1999-12
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
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.
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 Buchi outomate voor die modeltoetsprosedure. Verifiering geskied dan deur te toets of die produk van die Buchi outomaat en toestanddiagram van die ESML modelleeg is. Die algoritmes om Buchi outomate vanaf LTL formules te bou, die toestandgenerasie tegniek van die modeltoetser, en die algoritme om die produk van 'n Buchi 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.
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 Buchi outomate voor die modeltoetsprosedure. Verifiering geskied dan deur te toets of die produk van die Buchi outomaat en toestanddiagram van die ESML modelleeg is. Die algoritmes om Buchi outomate vanaf LTL formules te bou, die toestandgenerasie tegniek van die modeltoetser, en die algoritme om die produk van 'n Buchi 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.
Description
Dissertion (M.Sc.) -- University of Stellenbosch, 1999.
Keywords
Computer programs -- Verification, Programming languages (Electronic computers), Model checking, Dissertations -- Computer science