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.
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/19584 |
| Date | 02 1900 |
| Creators | Bezuidenhout, Johannes Abraham |
| Contributors | Geldenhuys, Jaco, Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. |
| Publisher | Stellenbosch : Stellenbosch University |
| Source Sets | South African National ETD Portal |
| Language | en_ZA |
| Detected Language | English |
| Type | Thesis |
| Format | viii, 99 leaves |
| Rights | Stellenbosch University |
Page generated in 0.0023 seconds