Efficiency issues in the design of a model checker

[摘要] ENGLISH SUMMARY: A model checker is a program that verifies, without human assistance, that the formal descriptionof a system has specified, desirable properties. The development of model checkingalgorithms is an active area of research, but most implementations are still prototypical in nature.In consequence, knowledge about the design and implementation of a practical, efficientmodel checker is limited.In this thesis the most important design decisions involved in creating an efficient on-the-flymodel checker are identified and discussed. In short, there are three major tasks:1. the generation of program states,2. the detection of revisited states, and3. the representation of states.In all three cases the central goal is to generate as many states as possible and to generatestates as fast as possible. For each task, alternatives are described and compared.The discussion of design issues is further supported in two ways. First, a detailed design andimplementation for a model checker is described to illustrate how design decisions affect eachother and ultimately the implementation. Second, the design arguments, based on more orless realistic models, are validated through a thorough study of the performance of the variouscomponents of the model checker.

[发布机构] Stellenbosch University