Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
An LTL verification system based on automata theory
Dissertion (M.Sc.) -- University of Stellenbosch, 1999.
Saved in:
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2012
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613762284945408 |
|---|---|
| access_status_str | Open Access |
| author | Inggs, Cornelia Petronella Van Wyk, Cornelia |
| author2 | De Villiers, P. J. A. |
| author_browse | De Villiers, P. J. A. Inggs, Cornelia Petronella Van Wyk, Cornelia |
| author_facet | De Villiers, P. J. A. Inggs, Cornelia Petronella Van Wyk, Cornelia |
| author_sort | Inggs, Cornelia Petronella |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Dissertion (M.Sc.) -- University of Stellenbosch, 1999. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/51128 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:41:16.700Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2012 |
| publishDateRange | 2012 |
| publishDateSort | 2012 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/51128 An LTL verification system based on automata theory Inggs, Cornelia Petronella Van Wyk, Cornelia De Villiers, P. J. A. Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer programs -- Verification Programming languages (Electronic computers) Model checking Dissertations -- Computer science Dissertion (M.Sc.) -- University of Stellenbosch, 1999. 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. 2012-08-27T11:34:20Z 2012-08-27T11:34:20Z 1999-12 Thesis http://hdl.handle.net/10019.1/51128 en_ZA Stellenbosch University 58 pages : ill. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Computer programs -- Verification Programming languages (Electronic computers) Model checking Dissertations -- Computer science Inggs, Cornelia Petronella Van Wyk, Cornelia An LTL verification system based on automata theory |
| title | An LTL verification system based on automata theory |
| title_full | An LTL verification system based on automata theory |
| title_fullStr | An LTL verification system based on automata theory |
| title_full_unstemmed | An LTL verification system based on automata theory |
| title_short | An LTL verification system based on automata theory |
| title_sort | ltl verification system based on automata theory |
| topic | Computer programs -- Verification Programming languages (Electronic computers) Model checking Dissertations -- Computer science |
| url | http://hdl.handle.net/10019.1/51128 |
| work_keys_str_mv | AT inggscorneliapetronella anltlverificationsystembasedonautomatatheory AT vanwykcornelia anltlverificationsystembasedonautomatatheory AT inggscorneliapetronella ltlverificationsystembasedonautomatatheory AT vanwykcornelia ltlverificationsystembasedonautomatatheory |