Thesis (MSc)--University of Stellenbosch, 2003. / ENGLISH ABSTRACT: Model checking is a computer-aided verification technique that is used to verify properties about the formal description of a system automatically. This technique has been applied successfully to detect subtle errors in reactive systems. Such errors are extremely difficult to detect by using traditional testing techniques. The conventional method of applying model checking is to construct a model manually either before or after the implementation of a system. Constructing such a model requires time, skill and experience. An alternative method is to derive a model from an implementation automatically. In this thesis two techniques of applying model checking to reactive systems are compared, both of which have problems as well as advantages. Two specific strategies are compared in the area of protocol development: 1. Structuring a protocol as a transition system, modelling the system, and then deriving an implementation from the model. 2. Automatically translating implementation code to a verifiable model. Structuring a reactive system as a transition system makes it possible to verify the control flow of the system at implementation level-as opposed to verifying the control flow at abstract level. The result is a closer correspondence between implementation and specification (model). At the same time testing, which is restricted to small, independent code fragments that manipulate data, is simplified significantly. The construction of a model often takes too long; therefore, verification results may no longer be applicable when they become available. To address this problem, the technique of automated model extraction was suggested. This technique aims to reduce the time required to construct a model by minimising manual input during model construction. A transition system is a low-level formalism and direct execution through interpretation is feasible. However, the overhead of interpretation is the major disadvantage of this technique. With automated model extraction there are disadvantages too. For example, differences between the implementation and specification languages-such as constructs present in the implementation language that cannot be expressed in the modelling language-make the development of an automated model extraction tool extremely difficult. In conclusion, the two techniques are compared against a set of software development considerations. Since a specific technique is not always preferable, guidelines are proposed to help select the best approach in different circumstances. / AFRIKAANSE OPSOMMING: Modeltoetsing is 'n rekenaargebaseerde verifikasietegniek wat gebruik word om eienskappe rakende 'n formele spesifikasie van 'n stelsel te verifieer. Die tegniek is al suksesvol toegepas om subtiele foute in reaktiewe stelsels op te spoor. Sulke foute word uiters moeilik opgespoor as tradisionele toetsings tegnieke gebruik word. Tradisioneel word modeltoetsing toegepas deur 'n model te bou voor of na die implementasie van 'n stelsel. Om'n model te bou verg tyd, vernuf en ervaring. 'n Alternatiewe metode is om outomaties 'n model van 'n implementasie af te lei. In hierdie tesis word twee toepassingstegnieke van modeltoetsing vergelyk, waar beide tegnieke beskik oor voordele sowel as nadele. Twee strategieë word vergelyk in die gebied van protokol ontwikkeling: 1. Om 'n protokol as 'n oorgangsstelsel te struktureer, dit te moduleer en dan 'n implementasie van die model af te lei. 2. Om outomaties 'n verifieerbare model van 'n implementasie af te lei. Om 'n reaktiewe stelsel as 'n oorgangsstelsel te struktureer maak dit moontlik om die kontrolevloei op implementasie vlak te verifieer-in teenstelling met verifikasie van kontrolevloei op 'n abstrakte vlak. Die resultaat is 'n nouer band wat bestaan tussen die implementasie en die spesifikasie. Terselfdetyd word toetsing, wat beperk word tot klein, onafhanklike kodesegmente wat data manupileer, beduidend vereenvoudig. Die konstruksie van 'n model neem soms te lank; gevolglik, wanneer die verifikasieresultate beskikbaar word, is dit dalk nie meer toepaslik op die huidige weergawe van 'n implementasie nie. Om die probleem aan te spreek is 'n tegniek om modelle outomaties van implementasies af te lei, voorgestel. Die doel van die tegniek is om die tyd wat dit neem om 'n model te bou te verminder deur handtoevoer tot 'n minimum te beperk. 'n Oorgangsstelsel is 'n laevlak formalisme en direkte uitvoering deur interpretasie is wesenlik. Die oorhoofse koste van die interpreteerder is egter die grootste nadeel van die tegniek. Daar is ook nadele wat oorweeg moet word rakende die tegniek om outomaties modelle van implementasies af te lei. Byvoorbeeld, verskille tussen die implementasietaal en spesifikasietaal=-soos byvoorbleed konstrukte wat in die implementasietaal gebruik word wat nie in die modeleringstaal voorgestel kan word nie-vrnaak die ontwikkeling van 'n modelafieier uiters moeilik. As gevolg word die twee tegnieke vergelyk teen 'n stel van programatuurontwikkelingsoorwegings. Omdat 'n spesifieke tegniek nie altyd voorkeur kan geniet nie, word riglyne voorgestel om te help met die keuse om die beste tegniek te kies in verskillende omstandighede.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: The search for non-terminating paths within a program is a crucial part of software verification, as the detection of anfinite path is often the only manner of falsifying program termination - the failure of a termination prover to verify termination does not necessarily imply that a program is non-terminating. This document describes the development and implementation of two focussed techniques for investigating the non-termination of affine loops. The developed techniques depend on the known non-termination concepts of recurrent sets and Jordan matrix decomposition respectively, and imply the decidability of single-variable and cyclic affine loops. Furthermore, the techniques prove to be practically capable methods for both the location of non-terminating paths, as well as the generation of preconditions for non-termination. / AFRIKAANSE OPSOMMING: Sagtewareveri kasie vereis of die bewys van die beeindiging van 'n program, of die deteksie van oneindige uitvoerings. In hierdie tesis ontwikkel en implementeer ons twee tegnieke om oor die oneindige eienskap van a ene lusse te beslis. Die tegnieke wat ontwikkel word is gebaseer op konsepte soos Jordan matriksdekomposisie en herhaalde groepe wat al in die verlede gebruik is om die beeindiging van lusse te ondersoek. Die tegnieke kan gebruik word om die uitvoerbaarheid van beide een-veranderlike en sikliese a ene lusse te bepaal. Feitlik alle nie-eindige a ene lusse kan ge denti seer word en die toestande waaronder hierdie oneindige eienskap verskyn kan beskryf word.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: The amount of information that users of social networks consume on a daily basis is steadily increasing. The resulting information overload is usually associated with a loss of control over the management of information sources, leaving users feeling overwhelmed. To address this problem, social networks have introduced tools with which users can organise the people in their networks. However, these tools do not integrate any automated processing. Twitter has lists that can be used to organise people in the network into topic-based groups. This feature is a powerful organisation tool that has two main obstacles to widespread user adoption: the initial setup time and continual curation. In this thesis, we investigate the problem of constructing topic-based Twitter lists. We identify two subproblems, an unsupervised and supervised task, that need to be considered when tackling this problem. These subproblems correspond to a clustering and classification approach that we evaluate on Twitter data sets. The clustering approach is evaluated using multiple representation techniques, similarity measures and clustering algorithms. We show that it is possible to incorporate a Twitter user’s social graph data into the clustering approach to find topic-based clusters. The classification approach is implemented, from a statistical relational learning perspective, with kLog. We show that kLog can use a user’s tweet content and social graph data to perform accurate topic-based classification. We conclude that it is feasible to construct useful topic-based Twitter lists with either approach. / AFRIKAANSE OPSOMMING: Die stroom van inligting wat sosiale-netwerk gebruikers op ’n daaglikse basis verwerk, is aan die groei. Vir baie gebruikers, skep hierdie oordosis inligting ’n gevoel dat hulle beheer oor hul inligtingsbronne verloor. As ’n oplossing, het sosiale-netwerke meganismes geïmplementeer waarmee gebruikers die inligting in hul netwerk kan bestuur. Hierdie meganismes is nie selfwerkend nie, maar kort toevoer van die gebruiker. Twitter het lyste geïmplementeer waarmee gebruikers ander mense in hul sosiale-netwerk kan groepeer. Lyste is ’n kragtige organiserings meganisme, maar tog vind grootskaal gebruik daarvan nie plaas nie. Gebruikers voel dat die opstelling te veel tyd in beslag neem en die onderhoud daarvan te veel moeite is. Hierdie tesis ondersoek die probleem om onderwerp-gerigte Twitter lyste te skep. Ons identisifeer twee subprobleme wat aangepak word deur ’n nie-toesig en ’n toesighoudende metode. Hierdie twee metodes hou verband met trosvorming en klassifikasie onderskeidelik. Ons evalueer beide die trosvorming en klassifikasie op twee Twitter datastelle. Die trosvorming metode word geëvalueer deur te kyk na verskillende voorstellingstegnieke, eendersheid maatstawwe en trosvorming algoritmes. Ons wys dat dit moontlik is om ’n gebruiker se Twitter netwerkdata in te sluit om onderwerp-gerigte groeperinge te vind. Die klassifikasie benadering word geïmplementeer met kLog, vanuit ’n statistiese relasionele leertoerie perspektief. Ons wys dat akkurate onderwerp-gerigte klassifikasie resultate verkry kan word met behulp van gebruikers se tweet-inhoud en sosiale-netwerk data. In beide gevalle wys ons dat dit moontlik is om onderwerp-gerigte Twitter lyste, met goeie resultate, te bou.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: Probabilistic symbolic execution is a new approach that extends the normal symbolic execution with probability calculations. This approach combines symbolic execution and model counting to estimate the number of input values that would satisfy a given path condition, and thus is able to calculate the execution probability of a path. The focus has been on programs that manipulate primitive types such as linear integer arithmetic in object-oriented programming languages such as Java. In this thesis, we extend probabilistic symbolic execution to handle data structures, thus allowing support for reference types. Two techniques are proposed to calculate the probability of an execution when the programs have structures as inputs: an approximate approach that assumes probabilities for certain choices stay fixed during the execution and an accurate technique based on counting valid structures. We evaluate these approaches on an example of a Binary Search Tree and compare it to the classic approach which only take symbolic values as input. / AFRIKAANSE OPSOMMING: Probabilistiese simboliese uitvoering is ’n nuwe benadering wat die normale simboliese uitvoering uitbrei deur waarksynlikheidsberekeninge by te voeg. Hierdie benadering kombineer simboliese uitvoering en modeltellings om die aantal invoerwaardes wat ’n gegewe padvoorwaarde sal bevredig, te beraam en is dus in staat om die uitvoeringswaarskynlikheid van ’n pad te bereken. Tot dus vêr was die fokus op programme wat primitiewe datatipes manipuleer, byvoorbeeld lineêre heelgetalrekenkunde in objek-geörienteerde tale soos Java. In hierdie tesis brei ons probabilistiese simboliese uitvoering uit om datastrukture, en dus verwysingstipes, te dek. Twee tegnieke word voorgestel om die uitvoeringswaarskynlikheid van ’n program met datastrukture as invoer te bereken. Eerstens is daar die benaderingstegniek wat aanneem dat waarskynlikhede vir sekere keuses onveranderd sal bly tydens die uitvoering van die program. Tweedens is daar die akkurate tegniek wat gebaseer is op die telling van geldige datastrukture. Ons evalueer hierdie benaderings op ’n voorbeeld van ’n binêre soekboom en vergelyk dit met die klassieke tegniek wat slegs simboliese waardes as invoer neem.

Thesis (MScEng (Electrical and Electronic Engineering))--University of Stellenbosch, 2005. / This project started a new research area in rotary-wing °ight control in the Computer and Control group at the University of Stellenbosch. Initial attempts to build a quad-rotor vehicle exposed di±culties which motivated changing to a standard model helicopter as a test vehicle. A JR Voyager E electrically powered model helicopter was instrumented with low-cost, low-weight sensors and a data communication RF link. The total cost of the sensor, communication and microcontroller hardware used is approximately US$ 1000 and the added onboard hardware weighs less than 0:4 kg. The sensors used to control the helicopter include a non-di®erential u-Blox GPS receiver, Analog Devices ADXRS150 rate gyroscopes, Analog Devices ADXL202 accelerometers, a Polaroid ultrasonic range sensor and a Honeywell HMC2003 magnetometer. Successful yaw, height and longitudinal position control was demonstrated. Signi¯cant further work is proposed, based on the literature study performed and the insights and achievements of the ¯rst rotary-wing unmanned aerial vehicle project in the group.

Thesis (MScIng)--University of Stellenbosch, 2003. / ENGLISH ABSTRACT: A complete mixed-potential integral equation formulation for the analysis of arbitrarily shaped scatterers in a planarly layered medium is presented. The integral equation is able to solve for simultaneous electric and magnetic surface currents using a Method of Moments (MoM) procedure. The MoM formulation which was developed uses vector-valued basis functions defined over a triangular mesh and are used to model electric currents on conducting scatterers and magnetic currents on slotline structures. The Green’s functions employed in the analysis were developed for a stratified medium using a Sommerfeld plane wave formulation. The scheme used for filling the method of moments matrix was designed to simultaneously solve multiple problems that are stacked and separated by an infinite conducting ground plane. The filling algorithm also efficiently packs partially symmetric matrices, which are present when solving problems that support a combination of electric and magnetic currents. Several examples are presented to illustrate and validate the analysis method. Numerical predictions of the scattering parameters (both magnitude and phase) show good correspondence with results from literature and measured data. / AFRIKAANSE OPSOMMING: ’n Volledige gemengde potensiaal integraalvergelyking formulering vir die analise van stralers van arbitrˆere vorm binne gelaagde strukture word aangebied. Die integraalvergelyking kan gelyktydige elektriese en magnetiese oppervlakstrome oplos deur die Metode van Momente (MoM) te gebruik. Die MoM formulering gebruik vektor basis funksies wat oor ’n driehoekige diskretisering gedefinieer word om elektriese strome op geleidende stralers en magnetiese strome op gleuflyn strukture te modelleer. Die Green’s funksies wat in die analise gebruik word, is ontwikkel vir gelaagde media deur gebruik te maak van Sommerfeld se platvlakgolf formulering. Die metode wat gebruik word om the moment matriks te vul, is ontwerp om meervoudige gestapelde probleme wat deur oneindig geleidende grondvlakke geskei word, gelyktydig op te los. Gedeeltelik simmetriese matrikse word ook effektief gevul. Hierdie matrikse kom voor wanneer probleme ’n kombinasie van elektriese en magnetiese strome ondersteun. Verskeie voorbeelde word gebruik om die analise metode te verifieer. Numeriese voorspellings van strooiparameters (beide grootte en hoek) vergelyk baie goed met resultate en gemete data wat in die literatuur gevind is. iv

Thesis (MScEng (Electrical and Electronic Engineering))--University of Stellenbosch, 2006. / This thesis is about the dynamic control of a permanent magnet assisted reluctance synchronous machine (PMA RSM). The PMA RSM in this thesis is a 110 kW traction machine and is ideal for the use in electrical rail vehicles. An application of the dynamic control of the PMA RSM in electrical rail vehicles is to reduce wheel slip. The mathematical model of the PMA RSM is derived and explained in physical terms. Two methods of current control for the PMA RSM are investigated, namely constant field current control (CFCC) and constant current angle control (CCAC). It is shown that CCAC is more appropriate for the PMA RSM. A current controller for the PMA RSM that guarantees stability is derived and given as an analytic formula. This current controller can be used for any method of current control, i.e. CFCC or CCAC. An accurate simulation model for the PMA RSM is obtained using results from finite element analysis (FEA). The accurate model is used in a simulation to verify CCAC. A normal proportional integral speed controller for the PMA RSM is designed and the design is also verified by simulation. Practical implementation of the current and speed controllers is considered along with a general description of the entire drive system. The operation of the resolver (for position measurement) is given in detail. Important safety measures and the design of the electronic circuitry to give protection are shown. Practical results concerning current and speed control are then shown. To improve the dynamic performance of the PMA RSM, a load torque observer with compensation current feedback is investigated. Two observer structures are considered, namely the reduced state observer and the full state observer. The derivation of the full state observer and the detail designs of the observer elements are given. The accurate simulation model of the PMA RSM is used to verify the operation of the observer structures and to evaluate the dynamic performance. Both observer structures are implemented practically and practical results are shown. One method of position sensorless control, namely the high frequency voltage injection method, is discussed in terms of the PMA RSM. This work is additional to the thesis but it is shown, because it raises some interesting questions regarding the dynamic control of the PMA RSM.

Transformation in education over the decades has failed to keep abreast of the rapidly advancing technological environment of modern society. This implies that curricula, learning paradigms and tools employed by educational institutions are not in sync with the technologically oriented lifestyle of modern society. Learners are therefore unable to apply and assimilate their daily life experiences into the learning process. This disparity warrants radical transformation in education, so as to furnish the appropriate education system where learners are able to construct their knowledge on the basis of pre-existing ideas and experiences. However, any transformation in the e~ucation approach should essentially be complemented by the adoption of appropriate learning environments and paradigms that can capitalize on learners' life experiences as well as elicit the appropriate learning behaviour and attitudes for effective and life-long learning. Much of the literature reviewed affirms the efficacy of virtual learning environments as mediums that can facilitate effective learner-centred electronic-learning suitable for modern society. They are asserted as liberators of learning in respect of instructivist ideals, information access and the confines of the physical classroom. This is confirmed by findings of this research, which are generally in favour of the virtual learning environment's ability to enhance the learning experiences of learners but remained inconclusive on their learning outcomes. / Thesis (M.Sc.)-University of Natal, Durban, 2003.

With the advent of globalisation and new communication technologies, it was inevitable that educational institutions would follow the advertising trend of establishing websites to market their services. This paper analyses the cultural and ideological values transmitted by such university websites. Particular focus is on issues around gender, sexual orientation, race, religion and socioeconomic status. The aim is to analyse consumer reaction to Internet messages conveyed in websites from different cultures, compare them with the intentions of producers and to relate all these back to ideological factors. This study deconstructs content and messages conveyed by University websites to assess the extent to which they might subscribe to particular ideologies (whether overt or covert). The argument that there are hidden ideologies in Web design does not imply that designers or producers intended any conspiracy or deception. Rather, the study compares the organisation's intended image/ethos with that which consumers perceive through their exposure to the website. The methodology was purposive sampling of participants consulted through personal (face-to-face) and interviews conducted online, as well as email-distributed questionnaires.This study uses websites of two universities in the KwaZulu-Natal region of South Africa. / Thesis (M.Sc.)-University of Natal, Durban, 2003.

A shock is essentially a propagating variation in the pressure or density of a medium. If the medium is transparent, such as air, and the shock radially symmetric, the refractive fringe diagnostic can be used to examine its general features. A laser beam probes the shock, the central part of the beam, refracted to different degrees by the different density features within the shock, interferes with itself and with the outer unrefracted part creating a series of coarse and fine fringes. By examining this interference pattern one can gain insight into the density profile underlying the shock. A series of such experiments was conducted by the Plasma Physics Research Institute at the University of Natal in 1990. To model the situation computationally, they developed a ray-tracer which produced interference patterns for modified theoretical density profiles based on those predicted by Sedov. After numerous trials, an intensity pattern was produced which agreed approximately with experimental observations. Thus encouraged, the institute then sought to determine density profiles directly from the interference patterns, but a true mathematical deconvolution proved non-trivial and is still awaited. The work presented in this thesis reconstructs the ray-tracer using software engineering techniques and achieves the desired deconvolution by training a neural network of the back-propagation type to behave as an inverse ray-tracer. The ray-tracer is first used to generate numerous density profile - interference pattern pairs. The neural network is trained with this theoretical data to provide a density profile when presented with an interference pattern. The trained network is then tested with experimental interference patterns extracted from captured images. The density profiles predicted by the neural network are then fed back to the ray-tracer and the resultant theoretically determined interference patterns compared to those obtained experimentally. The shock is examined at various times after the initial explosion allowing its propagation to be tracked by its evolving density profile and interference pattern. The results obtained prove superior to those first published by the institute and confirm the neural network's promise as a research tool. Instead of lengthy trial and error sessions with the unaided ray-tracer, experimental interference patterns can be fed directly to an appropriately trained neural network to yield an initial density profile. The network, not the researcher, does the pattern association. / Thesis (M.Sc.)-University of Natal, 1996.