Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Automated program generation : bridging the gap between model and implementation
Thesis (MSc)--University of Stellenbosch, 2007.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2012
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613965011386368 |
|---|---|
| access_status_str | Open Access |
| author | Bezuidenhout, Johannes Abraham |
| author2 | Geldenhuys, Jaco |
| author_browse | Bezuidenhout, Johannes Abraham Geldenhuys, Jaco |
| author_facet | Geldenhuys, Jaco Bezuidenhout, Johannes Abraham |
| author_sort | Bezuidenhout, Johannes Abraham |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--University of Stellenbosch, 2007. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/19584 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:44:30.757Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2012 |
| publishDateRange | 2012 |
| publishDateSort | 2012 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/19584 Automated program generation : bridging the gap between model and implementation Bezuidenhout, Johannes Abraham Geldenhuys, Jaco Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. Computer software -- Verification Theses -- Computer science Dissertations -- Computer science Thesis (MSc)--University of Stellenbosch, 2007. 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. 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. 2012-02-07T08:07:50Z 2012-02-07T08:07:50Z 2012-02 Thesis http://hdl.handle.net/10019.1/19584 en_ZA Stellenbosch University viii, 99 leaves application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Computer software -- Verification Theses -- Computer science Dissertations -- Computer science Bezuidenhout, Johannes Abraham Automated program generation : bridging the gap between model and implementation |
| title | Automated program generation : bridging the gap between model and implementation |
| title_full | Automated program generation : bridging the gap between model and implementation |
| title_fullStr | Automated program generation : bridging the gap between model and implementation |
| title_full_unstemmed | Automated program generation : bridging the gap between model and implementation |
| title_short | Automated program generation : bridging the gap between model and implementation |
| title_sort | automated program generation bridging the gap between model and implementation |
| topic | Computer software -- Verification Theses -- Computer science Dissertations -- Computer science |
| url | http://hdl.handle.net/10019.1/19584 |
| work_keys_str_mv | AT bezuidenhoutjohannesabraham automatedprogramgenerationbridgingthegapbetweenmodelandimplementation |