Thesis (MSc)--University of Stellenbosch, 2004. / ENGLISH ABSTRACT: Embedded computer systems form part of larger systems such as aircraft or chemical processing
facilities. Although testing and debugging of such systems are difficult, reliability is often
essential. Development of embedded software can be simplified by an environment that limits
opportunities for making errors and provides facilities for detection of errors. We implemented
a language and compiler that can serve as basis for such an experimental environment. Both
are designed to make verification of implementations feasible.
Correctness and safety were given highest priority, but without sacrificing efficiency wherever
possible. The language is concurrent and includes measures for protecting the address spaces
of concurrently running processes. This eliminates the need for expensive run-time memory
protection and will benefit resource-strapped embedded systems. The target hardware is
assumed to provide no special support for concurrency. The language is designed to be
small, simple and intuitive, and to promote compile-time detection of errors. Facilities for
abstraction, such as modules and abstract data types support implementation and testing of
bigger systems.
We have opted for model checking as verification technique, so our implementation language
is similar in design to a modelling language for a widely used model checker. Because of
this, the implementation code can be used as input for a model checker. However, since the
compiler can still contain errors, there might be discrepancies between the implementation
code written in our language and the executable code produced by the compiler. Therefore
we are attempting to make verification of executable code feasible. To achieve this, our
compiler generates code in a special format, comprising a transition system of uninterruptible
actions. The actions limit the scheduling points present in processes and reduce the different
interleavings of process code possible in a concurrent system. Requirements that conventional
hardware places on this form of code are discussed, as well as how the format influences
efficiency and responsiveness. / AFRIKAANSE OPSOMMING: Ingebedde rekenaarstelsels maak deel uit van groter stelsels soos vliegtuie of chemiese prosesseerfasiliteite.
Hoewel toetsing en ontfouting van sulke stelsels moeilik is, is betroubaarheid
dikwels onontbeerlik. Ontwikkeling van ingebedde sagteware kan makliker gemaak word met
'n ontwikkelingsomgewing wat geleenthede vir foutmaak beperk en fasiliteite vir foutbespeuring
verskaf. Ons het 'n programmeertaal en vertaler geïmplementeer wat as basis kan dien vir
so 'n eksperimentele omgewing. Beide is ontwerp om verifikasie van implementasies haalbaar
te maak.
Korrektheid en veiligheid het die hoogste prioriteit geniet, maar sonder om effektiwiteit prys
te gee, waar moontlik. Die taal is gelyklopend en bevat maatreëls om die adresruimtes van
gelyklopende prosesse te beskerm. Dit maak duur looptyd-geheuebeskerming onnodig, tot
voordeel van ingebedde stelsels met 'n tekort aan hulpbronne. Daar word aangeneem dat
die teikenhardeware geen spesiale ondersteuning vir gelyklopendheid bevat nie. Die programmeertaal
is ontwerp om klein, eenvoudig en intuïtief te wees, en om vertaaltyd-opsporing van
foute te bevorder. Fasiliteite vir abstraksie, byvoorbeeld modules en abstrakte datatipes,
ondersteun implementering en toetsing van groter stelsels.
Ons het modeltoetsing as verifikasietegniek gekies, dus is die ontwerp van ons programmeertaal
soortgelyk aan dié van 'n modelleertaal vir 'n modeltoetser wat algemeen gebruik word.
As gevolg hiervan kan die implementasiekode as toevoer vir 'n modeltoetser gebruik word.
Omdat die vertaler egter steeds foute kan bevat, mag daar teenstrydighede bestaan tussen die
implementasie geskryf in ons implementasietaal, en die uitvoerbare masjienkode wat deur die
vertaler gelewer word. Daarom poog ons om verifikasie van die uitvoerbare masjienkode haalbaar
te maak. Om hierdie doelwit te bereik, is ons vertaler ontwerp om 'n spesiale formaat
masjienkode te genereer bestaande uit 'n oorgangstelsel wat ononderbreekbare (atomiese) aksies
bevat. Die aksies beperk die skeduleerpunte in prosesse en verminder sodoende die aantal
interpaginasies van proseskode wat moontlik is in 'n gelyklopende stelsel. Die vereistes wat
konvensionele hardeware aan dié spesifieke formaat kode stel, word bespreek, asook hoe die formaat effektiwiteit en reageerbaarheid van die stelsel beïnvloed.
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/49823 |
| Date | 04 1900 |
| Creators | Swart, Riaan |
| Contributors | De Villiers, P. J. A., Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences (applied, computer, mathematics). |
| Publisher | Stellenbosch : Stellenbosch University |
| Source Sets | South African National ETD Portal |
| Language | en_ZA |
| Detected Language | English |
| Type | Thesis |
| Format | 104 p. : ill. |
| Rights | Stellenbosch University |
Page generated in 0.0026 seconds