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 (MSc)--University of Stellenbosch, 2001. / ENGLISH ABSTRACT: Computer-aided verification techniques, such as model checking, are often considered essential to produce highly reliable software systems. Modern model checkers generally require models to be written in eSP-like notations. Unfortunately, such systems are usually implemented using conventional imperative programming languages. Translating the one paradigm into the other is a difficult and error prone process. If one were to program in a process-oriented language from the outset, the chasm between implementation and model could be bridged more readily. This would lead to more accurate models and ultimately more reliable software. This thesis covers the definition of a process-oriented language targeted specifically towards embedded systems and the implementation of a suitable compiler and run-time system. The language, LF, is for the most part an extension of the language Joyce, which was defined by Brinch Hansen. Both LF and Joyce have features which I believe make them easier to use than other esp based languages such as occam. An example of this is a selective communication primitive which allows for both input and output guards which is not supported in occam. The efficiency of the implementation is important. The language was therefore designed to be expressive, but constructs which are expensive to implement were avoided. Security, however, was the overriding consideration in the design of the language and runtime system. The compiler produces native code. Most other esp derived languages are either interpreted or execute as tasks on host operating systems. Arguably this is because most implementations of esp and derivations thereof are for academic purposes only. LF is intended to be an implementation language. The performance of the implementation is evaluated in terms of practical metries such as the time needed to complete communication operations and the average time needed to service an interrupt. / AFRIKAANSE OPSOMMING: Rekenaar ondersteunde verifikasietegnieke soos programmodellering, is onontbeerlik in die ontwikkeling van hoogs betroubare programmatuur. In die algemeen, aanvaar programme wat modelle toets eSP-agtige notasie as toevoer. Die meeste programme word egter in meer konvensionele imperatiewe programmeertale ontwikkel. Die vertaling vanuit die een paradigma na die ander is 'n moelike proses, wat baie ruimte laat vir foute. Indien daar uit die staanspoor in 'n proses gebaseerde taal geprogrammeer word, sou die verwydering tussen model en program makliker oorbrug kon word. Dit lei tot akkurater modelle en uiteindelik tot betroubaarder programmatuur. Die tesis ondersoek die definisie van 'n proses gebaseerde taal, wat gemik is op ingebedde programmatuur. Verder word die implementasie van 'n toepaslike vertaler en looptyd omgewing ook bespreek. Die taal, LF, is grotendeels gebaseer op Joyce, wat deur Brinch Hansen ontwikkel is. Joyce en op sy beurt LF, is verbeterings op ander esp verwante tale soos occam. 'n Voorbeeld hiervan is 'n selektiewe kommunikasieprimitief wat die gebruik van beide toevoer- en afvoerwagte ondersteun. Omdat 'n effektiewe implementasie nagestreef word, is die taalontwerp om so nadruklik moontlik te wees, sonder om strukture in te sluit wat oneffektief is om te implementeer. Sekuriteit was egter die oorheersende oorweging in die ontwerp van die taal en looptyd omgewing. Die vertaler lewer masjienkode, terwyl die meeste ander implementasies van eSP-agtige tale geinterpreteer word of ondersteun word as prosesse op 'n geskikte bedryfstelsel- die meeste eSP-agtige tale word slegs vir akademiese doeleindes aangewend. LF is by uitstek ontwerp as implementasie taal. Die evaluasie van die stelsel se werkverrigting is gedoen aan die hand van praktiese maatstawwe soos die tyd wat benodig word vir kommunikasie, sowel as die gemiddelde tyd benodig vir die hantering van onderbrekings.

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.

Thesis (MSc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009. / Since the late 1990s, the Robot Soccer World Cup has been used as a testing ground for new technology in the eld of robotic design and arti cial intelligence. This research initiative pits two teams of robots against each other in a game of soccer. It is hoped that the technology gained will enable the construction of a fully autonomous team of robot players to play a normal soccer game against a human team by the year 2050. In robot soccer matches, as in real soccer matches, inferring an opponent's strategy can give a team a major advantage. One important aspect of a team's strategy is the formation the team uses. Knowing the formations that an opposing team tends to take, enables a team to prepare appropriate countermeasures. This thesis will investigate methods to extract formation information from a completed soccer game. The results show that these methods can be used to infer a classical team formation, as well as other distinguishing characteristics of the players, such as which areas on the eld the players tend to occupy, or the players' movement patterns - both valuable items of information for a future opposition team.

Thesis (MSc (Mathematical Sciences))-- University of Stellenbosch, 2010. / ENGLISH ABSTRACT: We investigate the suitability of applying some of the probabilistic and automata theoretic ideas, that have been extremely successful in the areas of speech and natural language processing, to the area of musical style imitation. By using music written in a certain style as training data, parameters are calculated for (visible and hidden) Markov models (of mixed, higher or first order), in order to capture the musical style of the training data in terms of mathematical models. These models are then used to imitate two instrument music in the trained style. / AFRIKAANSE OPSOMMING: Hierdie tesis ondersoek die toepasbaarheid van probabilitiese en outomaatteoretiese konsepte, wat uiters suksesvol toegepas word in die gebied van spraak en natuurlike taal-verwerking, op die gebied van musiekstyl nabootsing. Deur gebruik te maak van musiek wat geskryf is in ’n gegewe styl as aanleer data, word parameters vir (sigbare en onsigbare) Markov modelle (van gemengde, hoër- of eerste- orde) bereken, ten einde die musiekstyl van die data waarvan geleer is, in terme van wiskundige modelle te beskryf. Hierdie modelle word gebruik om musiek vir twee instrumente te genereer, wat die musiek waaruit geleer is, naboots.