Following the Second World War, the Food and Agriculture Organization (FAO) and the World Health Organization (WHO) teamed up to construct an international Codex Alimentarius (or “food code”) in 1962. Inspired by the work of its European predecessor, the Codex Europaeus, these two UN agencies assembled teams of health professionals, government civil servants, medical and scientific experts to draft food standards. Once ratified, the standards were distributed to governments for voluntary adoption and implementation. By the mid-1990s, the World Trade Organization (WTO) identified the Codex as a key reference point for scientific food standards. The role of science within this highly political and economic organization poses interesting questions about the process of knowledge production and the scientific expertise underpinning the food standards. Standards were constructed and contested according to the Codex twin goals of: (1) protecting public health, and (2) facilitating trade. One recent criticism of Codex is that these two aims are opposed, or that one is given primacy over the other, which results in protectionism. Bearing these themes in mind, in this dissertation I examine the relationship between the scientific and the ‘social’ elements embodied by the Codex food standards since its inception after the Second World War. I argue that these attempts to reach scientific standards represent an example of coproduction– one in which the natural and social orders are produced alongside each other. What follows from this central claim is an attempt to characterize the pre-WTO years of the Codex through a case study approach. The narrative begins with a description of the predecessor regional group the Codex europaeus, and then proceeds to key areas affecting human health: 1) food additives, 2) food hygiene, and 3) pesticides residues.

Cette thèse porte sur l’utilisation d’une langue contrôlée pour les spécifications des besoins du logiciel en thaï. L’étudedécrit les ambiguïtés syntaxiques et sémantiques ainsi que les problèmes rencontrés dans les spécifications des besoins dulogiciel en thaï. Ce travail explique également la nature de la langue thaïe. Le modèle de la langue contrôlée pour lesspécifications des besoins du logiciel en thaï, proposé dans cette étude, comprend trois composantes: l’analyse lexicale,l’analyse syntaxique et l’analyse sémantique. Pour l’analyse syntaxique, une syntaxe contrôlée est conçue en utilisant laforme du Backus-Naur (BNF). Quant à l’analyse lexicale, nous créons une ressource lexicale sous forme de langage XMLpour stocker tous les mots classés selon leur domaine. Les mots reçus de la ressource XML sont corrects d’un point de vueconceptuel mais ne sont pas pertinents d’un point de vue sémantique. Pour résoudre ce problème, nous faisons alors usage dematrices booléennes pour aligner les phrases sémantiquement. Ainsi les phrases produites par le modèle serontsyntaxiquement et sémantiquement correctes.Après avoir créé le modèle, nous avons construit un logiciel pour tester son efficacité. Il est ainsi évalué par quatreméthodes d’évaluation : 1. le test de fonctionnement syntaxique pour vérifier la syntaxe de la phrase; 2. le test defonctionnement sémantique pour tester la sémantique de la phrase; 3. le test d’acceptation en terme de satisfaction desutilisateurs avec le logiciel; et 4. le test d’acceptation en terme d’acception des données de sortie.Des résultats positifs montrent que : 1. les phrases produites par le modèle proposé sont syntaxiquement correctes; 2. lesphrases produites par le modèle proposé sont sémantiquement correctes; 3. les utilisateurs sont satisfaits et acceptent lelogiciel; et 4. les utilisateurs acceptent et comprennent les phrases produites par ce modèle. / This thesis focuses on using controlled language for Thai software requirements specifications. The studydescribes the ambiguities and problems encountered in Thai software requirements specifications; both syntacticambiguity and semantic ambiguity. The study also describes the nature of the Thai language. The model of controlledlanguage for Thai software requirements specifications is composed of three main components: lexical analysis,syntactic analysis, and semantic analysis. For syntactic analysis, a controlled syntax is created using Backus-NaurForm (BNF). In the lexical analysis stage, an XML format lexical resource is built to store words according to theirdomain. The words received from the XML resource are conceptually correct but may be semantically irrelevant. Tosolve this issue, the model applies Boolean Matrices to align sentences semantically. As a result, the sentencesproduced from the model are guaranteed to be syntactically and semantically correct.After having created this model, a program for testing the efficiency of the model is developed. The model isevaluated using four testing methods as follows: 1. functional testing for the correctness of the sentence’s syntax, 2.functional testing for the semantic correctness of the sentences produced by the model, 3. acceptance testing in termsof user satisfaction with the program, and 4. acceptance testing in terms of the validity of the outputs.The positive results signify that: 1. the sentences produced by the proposed model are syntactically correct, 2. thesentences produced by the proposed model are semantically correct, 3. the users are satisfied and accept the softwarecreated, and 4. the users approve and understand the sentences produced from this model.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Following the Second World War, the Food and Agriculture Organization (FAO) and the World Health Organization (WHO) teamed up to construct an international Codex Alimentarius (or “food code”) in 1962. Inspired by the work of its European predecessor, the Codex Europaeus, these two UN agencies assembled teams of health professionals, government civil servants, medical and scientific experts to draft food standards. Once ratified, the standards were distributed to governments for voluntary adoption and implementation. By the mid-1990s, the World Trade Organization (WTO) identified the Codex as a key reference point for scientific food standards. The role of science within this highly political and economic organization poses interesting questions about the process of knowledge production and the scientific expertise underpinning the food standards. Standards were constructed and contested according to the Codex twin goals of: (1) protecting public health, and (2) facilitating trade. One recent criticism of Codex is that these two aims are opposed, or that one is given primacy over the other, which results in protectionism. Bearing these themes in mind, in this dissertation I examine the relationship between the scientific and the ‘social’ elements embodied by the Codex food standards since its inception after the Second World War. I argue that these attempts to reach scientific standards represent an example of coproduction– one in which the natural and social orders are produced alongside each other. What follows from this central claim is an attempt to characterize the pre-WTO years of the Codex through a case study approach. The narrative begins with a description of the predecessor regional group the Codex europaeus, and then proceeds to key areas affecting human health: 1) food additives, 2) food hygiene, and 3) pesticides residues.

Incremental Dynamic Analysis (IDA) procedures are advanced and then applied to a quantitative risk assessment for bridge structures. This is achieved by combining IDA with site-dependent hazard-recurrence relations and damage outcomes. The IDA procedure is also developed as a way to select a critical earthquake motion record for a one-off destructive experiment. Three prototype bridge substructures are designed according to the loading and detailing requirements of New Zealand, Japan and Caltrans codes. From these designs 30 percent reduced scale specimens are constructed as part of an experimental investigation. The Pseudodynamic test is then to control on three specimens using the identified critical earthquake records. The results are presented in a probabilistic riskbased format. The differences in the seismic performance of the three different countries' design codes are examined. Each of these current seismic design codes strive for ductile behaviour of bridge substructures. Seismic response is expected to be resulting damage on structures, which may threaten post-earthquake serviceability. To overcome this major performance shortcoming, the seismic behaviour under bi-directional lateral loading is investigated for a bridge pier designed and constructed in accordance with Damage Avoidance principles. Due to the presence of steel armoured rocking interface at the base, it is demonstrated that damage can be avoided, but due to the lack of hysteresis it is necessary to add some supplemental damping. Experimental results of the armoured rocking pier under bi-directional loading are compared with a companion ductile design specimen.

Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5) Previous issue date: 2011-08-31 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++. / Usando m?todos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Al?m disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Por?m h? muita resist?ncia em se adotar essa abordagem de desenvolvimento de software. A raz?o principal e a escassez de suporte ferramental adequado, ?til e de f?cil utiliza??o. Os desenvolvedores normalmente escrevem o c?digo e o testam. Estes testes geralmente consistem em checar se as sa?das est?o de acordo com os requisitos. Isto, contudo, nem sempre e poss?vel de maneira exaustiva. Por outro lado, usando M?todos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especifica??o formal nem sempre possuem ferramentas como animador ou simulador e ?s vezes n?o h? interfaces gr?ficas amig?veis. Por?m, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transi??es Rotuladas (LTS). A proposta deste trabalho ? desenvolver um aplicativo que fornece anima??o gr?fica para especifica??es formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado ? poss?vel animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualiza??o de traces, escolhas feitas pelo usu?rio, em um formato de ?rvore gr?fica. A inten??o ? melhorar a compreens?o de uma especifica??o, fornecendo informa??es sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programa??o como Java e C++.

Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are: • Steap learning curve; formal techniques are said to be hard to use. • Lack of a step-by-step construction mechanism and poor guidance. • Difficulty to integrate the technique into the existing software processes. Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML. However, the case of coupling Object-Z (and also Z) and the Use Case Maps (UCMs) notation is still to be explored. A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored. The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software Requirements engineering process. / Computer Science / M. Sc. (Computer Science) / D. Phil. (Computer Science)

Theses (MTech (Business Information Systems))--Cape Peninsula University of Technology, 2016. / This paper describes the redesigning processes of the National Building Regulations of South Africa. These processes are administered by the National Regulator for Compulsory Specifications (NRCS) in terms of the National Building Regulations and Building Standards Act 103 of 1977 (The Act). The application of the business processes and the Building Control Officers from various local authorities nation-wide who enforce the National Building Regulations and Building Standards Act, 103 of 1977 (hereinafter referred to as “the Act”) with particular reference to implementation of core regulatory business processes within the building industry in Southern Africa. The investigation was largely motivated by the high number of injuries, deaths and/or human lives affected adversely and reported due to collapsing and defective buildings. These disasters occurred at various Local Authorities, in private residential homes, government-owned buildings, abandoned and commercial buildings, such as shopping malls, have been investigated and reported by the Building Regulator, i.e. the NRCS in collaboration with the Department of Labour’s Commission of Enquiry between the years 2012 and 2014. The reports show that in those sectors of building, the local authorities’ Building Control Officers, as the legislated enforcers of the Building Regulations (with the oversight role played by the NRCS), experienced the highest levels of non-compliance by various parties who are affected by the Building Regulations, i.e. building owners or their legal representatives, built-environment professional practitioners and builders. This study applies the interpretive approach underpinned by qualitative methodology where interviews were used to collect data from building owners, prospective building owners, building occupants, built-environment practitioners, Local Authorities’ building control officers and The Regulator of the National Building Regulations. The empirical findings revealed that there is a critical need for business process review and strategy shifts that advance objectivity and benefits to compliance, visibility and awareness of regulatory process, the highlights of possible endangerment of human life due to non-compliance, the outlining of sanctions for failure to comply, and stakeholder liaison. The output is a re-module of business processes that will enforce and maintain compliance of the building regulations of South Africa.

Para que o desenvolvimento de um novo produto tenha melhores chances de sucesso no competitivo mercado atual, as empresas devem preocupar-se em contemplar as reais necessidades dos clientes em seus projetos. Para tanto, é preciso que os desejos dos clientes transformem-se corretamente em especificações de produto claras e objetivas. Caso contrário, as incorretas ou subjetivas especificações-meta podem gerar um produto que não atenda às expectativas do consumidor. Sabe-se que o reprojeto e retrabalho para modificação do produto implicariam em perdas de tempo, custo e qualidade. Por isso, o processo de geração de especificações no desenvolvimento de produtos é crítico para atingir as metas de time-to-market, custo e qualidade do produto final. A tradução da voz do cliente em requisitos técnicos de projeto é, geralmente, realizada através de métodos como, por exemplo, o QFD. Contudo, o QFD não é muito utilizado na prática em diversos tipos de indústrias, como a de eletrodomésticos, devido a sua generalidade e dificuldade de uso. Desta forma, tem-se por objetivo principal desenvolver uma abordagem sistemática para auxiliar a elaboração de especificações-meta de um eletrodoméstico, no caso, um fogão. Foi realizada uma pesquisa de campo em uma empresa do ramo para a verificação da oportunidade de pesquisa e coleta de dados para o desenvolvimento de um método e ferramenta. Em seguida, elaborou-se uma ferramenta em planilha eletrônica na qual as especificações-meta de um fogão são geradas automaticamente a partir das informações de entrada de projeto. A validação da sistemática foi realizada pela análise comparativa do resultado gerado pela ferramenta com produtos anteriores já desenvolvidos pela empresa pesquisada. O resultado deste estudo indicou que o método proposto apresenta-se como um mecanismo para geração de especificações de maneira simples e prática, contribuindo para a maior assertividade no desenvolvimento do produto e possível de ser incorporado ao cotidiano da empresa. / In order for a new product development to have better chances of success in today’s competitive market, companies should focus on meeting the real consumer needs in their projects. Thus, it is necessary that the consumer wishes be transformed correctly into clear and objective product specifications. Otherwise, the incorrect or subjective target specifications could generate a product which does not fulfill to the consumer expectations. It is known that the redesign and rework needed due to product modifications would involve loss of time, cost and quality. So, the specification elaboration process during the product development is critical to achieve the targets as time-to-market, cost and quality of the final product. The translation of the voice of customer into project technical requirements is usually accomplished by such methods as, for example, QFD. However, the QFD is not used very often in several industries, like the home appliances factory, because it is general and difficult to use. Therefore, the main objective is to develop a systematic approach for a home appliance specification elaboration, in this case, a cooker. A field study was conducted in a company of this branch to verify the research opportunity and data collection for the method and tool development. Next, an electronic spreadsheet toll was developed for automatically generate the target specifications of a cooker from input data of the project. The systematic validation was implemented by the comparative analysis among the results obtained by the tool with previous products already developed by the researched company. The result of this study indicates that the method proposed is a mechanism for generating specifications in a simple and practical way, contributing to greater assertiveness in product development and can be embedded in the daily-basis process of the company.