A model checker for the LF system

[摘要] ENGLISH ABSTRACT: Computer aided veri cation techniques, such as model checking, can be used to improve thereliability of software. Model checking is an algorithmic approach to illustrate the correctnessof 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 allthe possible con gurations that these systems may exhibit. Traditionally model checking isapplied to abstract or high level designs of software. However, often interpreting or translatingthese abstract designs to implementations introduce subtle errors. In recent years onetrend in model checking has been to apply the model checking algorithm directly to theimplementations instead.This thesis is concerned with building an e cient model checker for a small concurrent langaugedeveloped at the University of Stellenbosch. This special purpose langauge, LF, isaimed at developement of small embedded systems. The design of the language was carefullyconsidered to promote safe programming practices. Furthermore, the language and its runtimesupport system was designed to allow directly model checking LF programs. To achievethis, the model checker extends the existing runtime support infrastructure to generate thestate space of an executing LF program.

[发布机构] Stellenbosch University