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 Author "Bezuidenhout, Johannes Abraham"

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    Automated program generation : bridging the gap between model and implementation
    (Stellenbosch : Stellenbosch University, 2012-02) Bezuidenhout, Johannes Abraham; Geldenhuys, Jaco; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science.
    ENGLISH ABSTRACT: The general goal of this thesis is the investigation of a technique that allows model checking to be directly integrated into the software development process, preserving the benefits of model checking while addressing some of its limitations. A technique was developed that allows a complete executable implementation to be generated from an enhanced model specification. This included the development of a program, the Generator, that completely automates the generation process. In addition, it is illustrated how structuring the specification as a transitions 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. By combining this structuring approach with automated implementation generation we ensure that the verified system behaviour is preserved in the actual implementation. An additional benefit is that data manipulation, which is generally not suited to model checking, is restricted to separate, independent code fragments that can be verified using verification techniques for sequential programs. These data manipulation code segments can also be optimised for the implementation without affecting the verification of the control structure. This technique was used to develop a reactive system, an FTP server, and this experiment illustrated that efficient code can be automatically generated while preserving the benefits of model checking.