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)

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.