Doctoral Degrees (Mathematical Sciences)

Permanent URI for this collection

https://scholar.sun.ac.za/handle/10019.1/852

Browse

Browsing Doctoral Degrees (Mathematical Sciences) by browse.metadata.advisor "Geldenhuys, J."

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    A model checker for the LF system
    (Stellenbosch : Stellenbosch University, 2007-03) Gerber, Erick D. B.; Geldenhuys, J.; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science.
    ENGLISH ABSTRACT: Computer aided veri cation techniques, such as model checking, can be used to improve the reliability of software. Model checking is an algorithmic approach to illustrate the correctness of temporal logic speci cations in the formal description of hardware and software systems. In contrast to traditional testing tools, model checking relies on an exhaustive search of all the possible con gurations that these systems may exhibit. Traditionally model checking is applied to abstract or high level designs of software. However, often interpreting or translating these abstract designs to implementations introduce subtle errors. In recent years one trend in model checking has been to apply the model checking algorithm directly to the implementations instead. This thesis is concerned with building an e cient model checker for a small concurrent langauge developed at the University of Stellenbosch. This special purpose langauge, LF, is aimed at developement of small embedded systems. The design of the language was carefully considered to promote safe programming practices. Furthermore, the language and its runtime support system was designed to allow directly model checking LF programs. To achieve this, the model checker extends the existing runtime support infrastructure to generate the state space of an executing LF program.