Automated program generation : bridging the gap between model and implementation
| dc.contributor.advisor | Geldenhuys, Jaco | |
| dc.contributor.author | Bezuidenhout, Johannes Abraham | |
| dc.contributor.other | Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. | en |
| dc.date.accessioned | 2012-02-07T08:07:50Z | |
| dc.date.available | 2012-02-07T08:07:50Z | |
| dc.date.issued | 2012-02 | |
| dc.description | Thesis (MSc)--University of Stellenbosch, 2007. | en_ZA |
| dc.description.abstract | 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. | en_ZA |
| dc.description.abstract | AFRIKAANSE OPSOMMING: Hierdie tesis ondersoek ’n tegniek wat modeltoetsing laat deel uitmaak van die sagtewareontwikkelingsproses, en sodoende betroubaarheid verbeter terwyl sekere tekorkominge van die tradisionele modeltoetsing proses aangespreek word. Die tegniek wat ontwikkel is maak dit moontlik om ’n volledige uitvoerbare implementasie vanaf ’n gespesialiseerde model spesifikasie te genereer. Om die implementasie-generasie stap ten volle te outomatiseer is ’n program, die Generator, ontwikkel. Daarby word dit ook gewys hoe die kontrolevloei op ’n formele manier geskei kan word van data-manipulasie deur gebruik te maak van ’n staatoorgangsstelsel struktureringsbenadering. Dit vereenvoudig die verifikasie proses, wat fokus op kontrolevloei. Deur di´e struktureringsbenadering te kombineer met outomatiese implementasie-generasie, word verseker dat die geverifieerde stelsel se gedrag behou word in die finale implementasie. ’n Bykomende voordeel is dat data-manipulasie, wat gewoonlik nie geskik is vir modeltoetsing nie, beperk word tot aparte, onafhanklike kode segmente wat geverifieer kan word deur gebruik te maak van verifikasie tegnieke vir sekwensi¨eele programme. Hierdie data-manipulasie kode segmente kan ook geoptimeer word vir die implementasie sonder om die verifikasie van die kontrole struktuur te be¨ınvloed. Hierdie tegniek word gebruik om ’n reaktiewe stelsel, ’n FTP bediener, te ontwikkel, en di´e eksperiment wys dat doeltreffende kode outomaties gegenereer kan word terwyl die voordele van modeltoetsing behou word. | af |
| dc.format.extent | viii, 99 leaves | |
| dc.identifier.uri | http://hdl.handle.net/10019.1/19584 | |
| dc.language.iso | en_ZA | en_ZA |
| dc.publisher | Stellenbosch : Stellenbosch University | |
| dc.rights.holder | Stellenbosch University | en_ZA |
| dc.subject | Computer software -- Verification | en_ZA |
| dc.subject | Theses -- Computer science | en_ZA |
| dc.subject | Dissertations -- Computer science | en_ZA |
| dc.title | Automated program generation : bridging the gap between model and implementation | en_ZA |
| dc.type | Thesis | en_ZA |