Automated program generation : bridging the gap between model and implementation

[摘要] ENGLISH ABSTRACT: The general goal of this thesis is the investigation of a technique that allows model checking tobe directly integrated into the software development process, preserving the benefits of modelchecking while addressing some of its limitations. A technique was developed that allows acomplete executable implementation to be generated from an enhanced model specification.This included the development of a program, the Generator, that completely automatesthe generation process. In addition, it is illustrated how structuring the specification as atransitions system formally separates the control flow from the details of manipulating data.This simplifies the verification process which is focused on checking control flow in detail. Bycombining this structuring approach with automated implementation generation we ensurethat the verified system behaviour is preserved in the actual implementation. An additionalbenefit is that data manipulation, which is generally not suited to model checking, is restrictedto separate, independent code fragments that can be verified using verification techniques forsequential programs. These data manipulation code segments can also be optimised for theimplementation without affecting the verification of the control structure. This techniquewas used to develop a reactive system, an FTP server, and this experiment illustrated thatefficient code can be automatically generated while preserving the benefits of model checking.

[发布机构] Stellenbosch University