This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.

Thesis (MA)--Stellenbosch University, 2000. / ENGLISH ABSTRACT: In the early 1970s the National Party government under B.l Vorster experienced serious problems due to its policy on the Coloured population. Issues concerning the mutual relations between the population groups came strongly to the fore and the government's policy of separate development was subject to widespread and severe criticism. The period 1970-1974 is generally regarded as a time of change in South Afiica due to international and foreign pressures. South Afiica's position in the international community deteriorated dramatically and attitudes towards the Republic became increasingly hostile in the rest of the world. Furthermore, the Vorster government was confronted with two opposing schools of thought within the party itself, the so-called verligtes and the verkramptes. During the 1970s the political decision-making processes became entangled in a continuous struggle between the enlightened wing of the National Party, the so-called Cape Liberals, and a more conservative element, the verkramptes of the Transvaal. Race relations issues and the government's Coloured policy in particular were often the source of contention. In March 1973 Vorster appointed a Commission of Enquiry into Matters Relating to the Coloured Population Group. It was chaired by prof Erika Theron, formerly professor in Social Work at the University of Stellenbosch. The Theron Commission, as it became known generally, consisted of twenty members, six of whom were Coloureds. The Commission had to investigate the following: the progress made by the Coloured population group since 1960 in the social, economic and constitutional spheres as well as in the fields of local management, culture and sport; constraining factors in the various fields that could be identified as sources of contention; and any other related matters. The Theron Commission's report was tabled in parliament three years later on 18 June 1976. The Soweto riots that broke out two days before, however, forced news of the report out of the newspapers and caused its influence to be largely dissipated. The Theron report contained a number of recommendations that were directly in conflict with the government's apartheid policy and were hence not acceptable to the government. Consequently, the government - by way of an interim memorandum and a later white paper - rejected those recommendations that affected the core of its apartheid policy. The recommendations included the repeal of the Mixed Marriages Act (Act 55 of 1949) and Section 16 of the Immorality Act (Act 23 of 1957), two of the cornerstones of the policy of apartheid. Recommendation No. 178, in which the commission recommended direct representation for Coloureds at the various levels of government, was also rejected by the government. The potential influence of the Theron Commission's report to influence change was thus firmly nipped in the bud. The government's reaction caused bitter disappointment among the Coloured population as well as enlightened Whites and at the same time fuelled the conflict between the verligtes and the verkramptes. It also ensured intensified criticism from the opposition parties, especially the United Party. Yet the recommendations of the Theron Commision's report played a prominent role in the late 1970s and early 1980s, when the wheels of political change began to tum, and let to the tricameral parliamentary system of 1984 in which the Coloured population group was also represented. The Arbeidersparty of South Africa (APSA) - Ministers' Council, which was in control of the House of Representatives from 1984 to 1992, consistently endeavoured to negotiate a better social, economic and constitutional position for the Coloured population on the basis of the Theron Commission's report. / AFRIKAANSE OPSOMMING: In die vroeë sewentigerjare van die twintigste eeu het die Nasionale Party-regering, onder die bewind van BJ. Vorster, ernstige probleme ten opsigte van sy Kleurlingbeleid ondervind. Probleme rondom die bevolkingsverhoudingsvraagstuk het sterk op die voorgrond getree en die regering se beleid van afsonderlike ontwikkeling aan wydverspreide en hewige kritiek onderwerp. Die tydperk 1970-1974 word allerweë deur kritici beskou as 'n tydperk van verandering in Suid-Afrika vanweë toenemende binne- en buitelandse druk. Suid-Afrika se posisie binne die internasionale gemeenskap het drasties verswak en die buiteland het 'n vyandige gesindheid jeens die Republiek geopenbaar. Daarbenewens het die Vorster-regering gebuk gegaan onder twee botsende denkrigtings binne die partygeledere, die sogenaamde verligtes en die verkramptes. Die politieke besluitnemingsprosesse van die sewentigerjare was vasgevang tussen die verligte vleuel van die Nasionale Party, die sogenaamde Cape Liberals, en 'n meer konserwatiewe element, die verkramptes van Transvaal tussen wie daar 'n voortdurende stryd gewoed het. Die bevolkingsverhoudingsvraagstuk en die regering se Kleurlingbeleid was gereeld in die spervuur. In Maart 1973 het Vorster 'n Kommissie van Ondersoek na Aangeleenthede rakende die Kleurlingbevolkingsgroep aangestel. Die voorsitter was prof Erika Theron, voormalige hoogleraar in Maatskaplike Werk aan die Universiteit van Stellenbosch. Die Theronkommissie, soos dit algemeen bekend sou staan, is saamgestel uit twintig lede waaronder ses Kleurlinge. Die kommissie moes ondersoek instel na die volgende: die vordering van die Kleurlingbevolkingsgroep sedert 1960 op maatskaplike, ekonomiese en staatkundige gebied asook op die terreine van plaaslike bestuur, kultuur en sport; stremmende faktore op die verskillende terreine wat as knelpunte geïdentifiseer kon word; en enige verdere verwante sake. Die Theron-verslag is drie jaar later op 18 Junie 1976 in die parlement ter tafel gelê. Die Soweto-onluste wat twee dae tevore uitgebreek het, het egter die verslag van die persblaaie verdring en die invloed daarvan grootliks verlore laat gaan. Die Theron-verslag het aanbevelings bevat wat lynreg in stryd was met die apartheidsbeleid en wat nie vir die regering aanneemlik was nie. Gevolglik het die regering by wyse van 'n tussentydse memorandum en 'n latere witskrif daardie aanbevelings wat die kern van sy apartheidsbeleid aangetas het, afgekeur. Onder die aanbevelings was die herroeping van die Wet op die Verbod van Gemengde Huwelike (Wet No. 55 van 1949) en Artikel 16 van die Ontugwet (Wet No. 23 van 1957), twee van die hoekstene van die apartheidsbeleid. Aanbeveling No. 178, waarin die kommissie regstreekse verteenwoordiging vir die Kleurlinge op die verskillende owerheidsvlakke en in besluitnemingsprosesse aanbeveel het, is ook deur die regering afgekeur. Sodoende is die Theron-verslag se potensiële invloed tot verandering in die kiem gesmoor. Die regering se reaksie het bittere teleurstelling onder die Kleurlinge en die verligte blankes veroorsaak en terselfdertyd die fel stryd tussen die verligtes en die verkramptes aangewakker. Dit het ook toenemende kritiek komende van die opposisiepartye, veral die Verenigde Party, op die regering verseker. Die aanbevelings van die Theron-verslag het nietemin 'n prominente rol gespeel in die laat sewentigerjare en vroeë tagtigerjare toe die wiel van politieke veranderinge begin draai het en uitgeloop het op die Driekamerparlementstelsel van 1984 waarbinne die Kleurlinge ook verteenwoordig was. Die Arbeidersparty van Suid-Afrika (APSA) - Ministersraad wat sedert 1984 tot 1992 in beheer van die Raad van Verteenwoordigers binne die Driekamerparlement was, het hom voortdurend beywer om aan die hand van die Theronverslag, 'n beter sosiale, ekonomiese en staatkundige posisie vir die Kleurlinge te beding.

Cultural heritage events as a tourism product have increased in recent years, both globally and in South Africa. Within the sphere of cultural heritage tourism, people construct and present their heritage and traditions to tourists in a reconstructed setting. To the visitors and people who are directly involved with the planning of the event, a sense of belonging and group identity are experienced by linking the present to the past in a celebratory mood. The annual ‘Afrikaanse Taal en Kultuurvereniging’ (ATKV) Riel Dance Competition in South Africa is an example of such an event, which celebrates a threatened cultural heritage in the form of a competition. The idea of a dance competition in order to preserve cultural heritage started in response to a feeling of marginalisation of culture among certain segments of the Coloured community of South Africa after the establishment of democracy in 1994. This dissertation used the constructivist-interpretivist approach in geographical enquiry to explain the role of cultural heritage events. Multiple sources of evidence and information were used in this study, including focus group interviews, observations, audio-visual materials, questionnaires and participant observation. The participants and visitors alike felt that the ATKV Riel Dance Competition serves an important role in preserving and protecting the cultural heritage of the Coloured community. The competition played a role in fulfilling the need of a large percentage of its participants and visitors for a group identity. There was no significant financial benefit for the communities who participated in the ATKV Riel Dance Competition. However, on a political level the competition played an important role in nation-building and cultural expression in South Africa. / Geography / M.A. (Geography)

Made available in DSpace on 2015-05-08T14:53:27Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 2050762 bytes, checksum: d03ea0191257aa516c9df03c51af0335 (MD5) Previous issue date: 2011-09-26 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This study proposes a systematic method for evaluating the performance of service delivery through process modeling and failure analysis. The implementation of the proposal took place in a distribution company of electricity (COELCE), in which he was elected New Process Connections as an object of study for the following reasons: This process helps to reduce the deficit of households without electricity in the country and showed a high rate of irregularities pointed out by regulators from providing that service here has to justify the choice of process and not the company. This is a case study, with secondary data were collected in books, websites, internal documents COELCE and scientific publications (journals, dissertations and theses). We obtained the primary data in reading and statistical analysis of company documents to the investigator assigned by the managers of the process, meetings with experts COELCE before, during and after field research, and intensive direct observation of the teams responsible for the physical connections of the units consumers. The methodology proposed by the tool is composed of colored Petri nets for modeling process New Links and techniques of failure analysis (FTA Fault Tree Analysis) and FMEA (Failure Mode and Effects Analysis). The systematic validation enabled: first - viewing different phases and activities of the process; second - identification of critical functions and potential failure of the process, the third - the formulation of action plan by the researcher to improve the process of New Connections. The action plan was endorsed by the group of experts COELCE, which collaborates with the research, from the exploratory phase. The use of integrated techniques proposed in this paper contributes to scientific knowledge by using the approach of process modeling and analysis techniques of failures in service businesses, especially in regard to the reduced number of work in this area. It is noteworthy that the systematics can be applied to other companies in the services sector can contribute in improving the performance of the processes analyzed. / Este estudo propõe uma sistemática para avaliar o desempenho da prestação de serviços por meio da modelagem de processos e análise de falha. A aplicação da proposta ocorreu em uma empresa de distribuição de energia elétrica (COELCE), na qual elegeu-se o Processo de Novas Ligações como objeto de estudo pelos seguintes motivos: esse processo contribui para reduzir o déficit de domicílios sem energia elétrica no país e apresentava elevado índice de irregularidades apontadas pelos órgãos reguladores da prestação desse serviço público. Trata-se de um estudo de caso cujos dados secundários foram coletados em livros, sites, documentos internos da COELCE e publicações científicas (periódicos, dissertações e teses). Obteve-se os dados primários em leitura e tratamento estatístico de documentos da empresa cedidos ao pesquisador pelos gestores do processo, reuniões com especialistas da COELCE, antes, durante e após pesquisa de campo, e observação direta intensiva das equipes responsáveis pelas ligações físicas das unidades consumidoras. A sistemática proposta é composta pela ferramenta redes de Petri Coloridas para modelagem do Processo de Novas Ligações e as técnicas de análise de falhas FTA (Fault Tree Analysis) e FMEA (Failure Mode and Effects Analysis). A validação da sistemática permitiu: primeiro - visualização de diferentes fases e atividades do processo; segundo identificação de funções críticas e falhas potenciais do processo; terceiro - formulação de plano de ação pelo pesquisador para melhoria do Processo de Novas Ligações. O plano de ação foi validado pelo grupo de especialistas da COELCE, que colabora com a pesquisa, desde a fase exploratória. A utilização das técnicas de forma integrada proposta neste trabalho contribui para o conhecimento científico por utilizar a abordagem de modelagem de processos e técnicas de análise de falhas em empresas de serviço, principalmente no que tange ao reduzido número de trabalho nesta área. Vale ressaltar que a sistemática pode ser aplicada em outras empresas do setor de serviços podendo contribuir na melhoria do desempenho dos processos analisados.

Made available in DSpace on 2015-03-03T15:08:46Z (GMT). No. of bitstreams: 1 RicardoWA.pdf: 1646499 bytes, checksum: efcc744c6ff7cea26befa0adbedb8c6a (MD5) Previous issue date: 2005-09-02 / Este trabalho apresenta uma t?cnica de verifica??o formal de Sistemas de Racioc?nio Procedural, PRS (Procedural Reasoning System), uma linguagem de programa??o que utiliza a abordagem do racioc?nio procedural. Esta t?cnica baseia-se na utiliza??o de regras de convers?o entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, s?o apresentadas regras de convers?o de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verifica??o formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verifica??o das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional dispon?vel para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de convers?o PRS-RPC, podemos ser levados a querer fazer esta convers?o de maneira estritamente manual. No entanto, a probabilidade de introdu??o de erros na convers?o ? grande, fazendo com que o esfor?o necess?rio para garantirmos a corretude da convers?o manual seja da mesma ordem de grandeza que a elimina??o de eventuais erros diretamente no programa PRS original. Assim, a convers?o automatizada ? de suma import?ncia para evitar que a convers?o manual nos leve a erros indesej?veis, podendo invalidar todo o processo de convers?o. A principal contribui??o deste trabalho de pesquisa diz respeito ao desenvolvimento de uma t?cnica de verifica??o formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de convers?o de PRS para RPC. A segunda fase ? concernente ao desenvolvimento de um conversor para fazer a transforma??o de maneira automatizada dos programas PRS para as RPCs. A convers?o autom?tica ? poss?vel, porque todas as regras de convers?o apresentadas seguem leis de forma??o gen?ricas, pass?veis de serem inclu?das em algoritmos

Personality and individual differences in reactions of the Great tit to aposematic prey were investigated. The aim of this study was to assess differences in personality of forty Great tits and find out possible correlation to the reactions of these birds to aposematic prey, the fifth larval instar of firebug Pyrrhocoris apterus.

Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework

With both a heterogeneous population and a large number of unidentified persons in South Africa, an accurate method to estimate ancestry is needed. The purpose of this study was to evaluate variation in nasal aperture shape in black, white and coloured South Africans, using linear measures and geometric morphometrics (GM), the latter which includes both procrustes analysis (GPA) and elliptical fourier analysis (EFA). To test statistical significance among groups, discriminant function analysis (DFA) and principal component analysis (PCA) was used. A total of 310 (164 male, 145 female) crania of black, white and coloured South Africans were used. Thirteen standard landmarks, namely, glabella, nasion, nasale superior, dacryon, nasale inferius, alare, most inferior nasal border and subspinale, were digitised with a MicroScribe G2™ (Immersion: San Jose, CA). Five linear measures, nasion-dacryon angle (NDA), nasal breadth (NLB), nasal height (NLH), inter-orbital breadth (DKB) and nasion-dacryon subtense (NDS), were calculated. For EFA, photographs were taken in a frontal plane of skulls that had been positioned in the Frankfort horizontal plane on a craniophore. All classification accuracies for all groups were better than chance. Using linear measures and GPA, black South Africans classified 55-71% correctly, coloured classified 53-61% correctly and whites classified 85-95% correctly. Black and coloured South Africans demonstrated bell-shaped nasal apertures with nasal spines superior to the inferior nasal border. White South Africans had pear-shaped nasal apertures with a nasal spine inferior of the inferior nasal border. Using EFA black South Africans classified 62% correctly. While coloured South Africans only classified 39% correctly, which demonstrates high within group variability. Due to their unique historical development, large variation (heterogeneity) within the coloured group was expected. White South Africans had the highest correct classification accuracy of 85%. For all methods, misclassification rarely occurred between white and non-white (black and coloured) groups and most difficulties arose in distinguishing non-white groups from each other. High rates of misclassification was also noted between sex designations within a group, which suggests less or an absence of sexual dimorphism for these variables The distinct separation of white South Africans may reflect the mid-to late 20th century political and social separation of white and non-white groups in South Africa. Nasal aperture shape, alone, is less useful for separating groups such that all groups have relatively intermediate nasal aperture shapes; however the pinched nasal bone structure of white South Africans clearly separates them from the other groups. When using nasal bone and aperture landmarks, linear measures are as accurate as the modern geometric techniques in distinguishing groups. All methods are feasible to use in the estimation of ancestry on modern South Africans, with craniometry a sensible solution as the data can be rapidly collected, accurately analysed and compared to current reference samples. Copyright / Dissertation (MSc)--University of Pretoria, 2012. / Anatomy / unrestricted

O uso de técnicas e métodos formais contribui para o desenvolvimento de sistemas confiáveis. No entanto, apesar do rigor obtido, em geral, é necessário que essas técnicas sejam complementadas com atividades de teste e validação. Deve-se ressaltar que o custo para eliminar erros encontrados nas etapas iniciais de desenvolvimento é menor do que quando esses erros são encontrados nas fases posteriores. Dessa forma, é essencial a condução de atividades de VV&T - Verificação, Validação e Teste - desde as primeiras fases de desenvolvimento. Critérios de teste, como uma forma sistemática de avaliar e/ou gerar casos de teste de qualidade e, dessa forma, contribuir para aumentar a qualidade da atividade de teste, têm sido investigados para o teste de especificação de Sistemas Reativos. A técnica Redes de Petri Coloridas tem sido constantemente utilizada para a especificação do aspecto comportamental de Sistemas Reativos. Apesar de existirem diversas técnicas de análise, um aspecto não considerado é a cobertura alcançada, visto que, em geral, a aplicação exaustiva não é viável devido ao alto custo. Considerando a relevância do estabelecimento de métodos sistemáticos para o teste e validação dessas especificações, este trabalho propõe a aplicação do critério de teste Análise de Mutantes para o teste de Redes de Petri Coloridas. Neste trabalho foram almejados três objetivos principais, os quais podem ser divididos em estudos teóricos, estudos empíricos e automatização. No contexto de estudos teóricos, foi realizada a definição e embasamento teórico para possibilitar a aplicação da Análise de Mutantes no contexto de Redes de Petri Coloridas. Além disso, investigaram-se mecanismos genéricos para a descrição e geração de mutantes. Definiu-se um algoritmo para a geração de casos de teste baseado na Análise de Mutantes. No contexto de estudos empíricos, foram conduzidos estudos de caso para avaliar a aplicabilidade e eficácia dos resultados teóricos obtidos. Finalmente, no contexto de automatização, foram desenvolvidas ferramentas de apoio à aplicação da Análise de Mutantes. / The usage of formal methods and techniques contributes to the development of highly reliable system, but, in spite of the achieved rigour, these techniques must be complemented with testing and validation activities. It should be highlighted that the cost to eliminate errors found in the early phases of development is smaller than when those errors are found in the later phases. Therefore, the accomplishment of VV&T activities - Verification, Validation and Test - starting at the first development phases is essential. Testing criteria, as a systematic way to evaluate and/or generate test cases, contributing, therefore, to improve the quality of the test activity, have been proposed for testing reactive systems specifications. A technique that has been steadily employed for specifying the behavioural aspect of reactive systems is the coloured Petri nets. Although there are several analysis and validation techniques, a usually neglected aspect is the achieved coverage, given that, in general, the exhaustive application is not feasible due to its high cost. Considering the relevance of establishing systematic methods for the test and validation of coloured Petri nets based specification, this work proposes the investigation of the viability of applying Mutation Testing to test coloured Petri nets. In this work three main goals were pursued, which can be grouped in: theoretical studies, empirical studies and tool development. In the context of theoretical studies, it was accomplished the definition of theoretical concepts to enable the application of Mutant Analysis in the context of coloured Petri nets. Moreover, a mutation-based algorithm was defined to generate test sequences for Petri nets. In the context of empirical studies, case studies were carried out to evaluate the applicability and effectiveness of the achieved theoretical results. Finally, in the context of tool development, tools for supporting the application of Mutation Testing were developed.

Magister Artium (Development Studies) - MA(DVS) / This study reflects the vital role the church should play in the social transformation of society. It undoubtedly has the potential to be a strategic organisation for social change. However, in the past it has failed to reach that potential. The hope for the future is that the church will embrace that potential and become active in the process of social transformation. The Church of the Province of Southern Africa (CPSA) has been the researcher's spiritual home for her entire life. During this time, and particularly over the past five years, she has sought to find her place in the church's inflexible, bureaucratic and patriarchal structure. While this study was in the final stages of being written, the CPSA took the historic decision to ordain women to the priesthood. Her personal struggle had been vindicated. However, more importantly, the church's decision attests to that organisation's potential for creative change. Thus this study is dedicated to the members of the CPSA in the Diocese of Cape Town, in the hope that they will embrace the challenge, both as individuals and as a community to become active agents of social change. The field research was conducted during the period March 1989 to March 1990 by the researcher herself, who was a paid employee of the Diocese of Cape Town at the time. Both the promoter and co-promoter of this thesis supervised this research. The results were first published in August 1990 by the Diocese of Cape Town in a report entitled, Voices of the Church: An Anglican perspective on welfare and development in the Diocese of Cape Town. Permission to use the research material in this study has been granted by the Most Reverend Desmond Mpilo Tutu, and is acknowledged with thanks. There are many people who during that period enabled the research to take place because of their willingness, enthusiasm and interest: the Most Reverend Desmond Tutu; Bishop Edward the liaison Bishop; members of Chapter and Diocesan Council; the support committee; the 130 people in the parishes who so willingly shared of themselves and their opinions, and in many instances opened their homes; and the clergy of the diocese, who participated wholeheartedly in the process.