abstract / toc / Computer Science and Information Systems / Doctoral / Doctor of Philosophy

One of the main objectives of software development in scientific computing is efficiency. Being focused on highly specialized application domain, important software quality metrics, e.g., usability, extensibility ,etc may not be amongst the list of primary objectives. In this research, we have studied the design structures and iterative releases of scientific research software using Design Structure Matrix(DSM). We implemented a DSM partitioning algorithm using sparse matrix data structure Compressed Row Storage(CRS), and its timing was better than those obtained from the most widely used C++ library boost. Secondly, we computed several architectural complexity metrics, compared releases and total release costs of a number of open source scientific research software. One of the important finding is the absence of circular dependencies in studied software which attributes to the strong emphasis on computational performance of the code. Iterative release analysis indicates that there might be a correspondence between “clustering co-efficient” and “release rework cost” of the software. / x, 87 leaves : ill. ; 29 cm

Testing statistics state that testing consumes more than half of a programmer's professional life, although few programmers like testing, fewer like test design and only 5% of their education will be devoted to testing. The main goal of this research is to test the efficiency of two software testing tools. Two experiments were conducted in the Computer Science Department at Ball State University. The first experiment compares two conditions - testing software using no tool and testing software using a command-line based testing tool - to the length of time and number of test cases needed to achieve an 80% statement coverage for 22 graduate students in the Computer Science Department. The second experiment compares three conditions - testing software using no tool, testing software using a command-line based testing tool, and testing software using a GUI interactive tool with added functionality - to the length of time and number of test cases needed to achieve 95% statement coverage for 39 graduate and undergraduate students in the same department. / Department of Computer Science

This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software.

No description available.

No description available.

Real applications of near-term quantum computing are around the corner and quantum software is a key component. Unlike classical computing, quantum software is under the threat of both quantum hardware errors and human bugs due to the unintuitiveness of quantum physics theory. Therefore, trustworthiness and reliability are critical for the success of quantum computation. However, most traditional methods to ensure software reliability, like testing, do not transfer to quantum at scale because of the destructive and probabilistic nature of quantum measurement and the exponential-sized state space. In this thesis, I introduce a series of frameworks to ensure the trustworthiness of quantum computing software by automated formal verification. First, I present Giallar, a fully-automated verification toolkit for quantum compilers to formally prove that the compiler is bug-free. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, I implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. The evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance. Second, I introduce Gleipnir, an error analysis framework for quantum programs that enable scalable and adaptive verification of quantum error through the application of tensor networks. Giallar introduces the ( 𝜌̂, 𝛿)-diamond norm, an error metric constrained by a quantum predicate consisting of the approximate state 𝜌̂ and its distance 𝛿 to the ideal state 𝜌. This predicate ( 𝜌̂, 𝛿) can be computed adaptively using tensor networks based on Matrix Product States. Giallar features a lightweight logic for reasoning about error bounds in noisy quantum programs, based on the ( 𝜌̂, 𝛿)-diamond norm metric. The experimental results show that Giallar is able to efficiently generate tight error bounds for real-world quantum programs with 10 to 100 qubits, and can be used to evaluate the error mitigation performance of quantum compiler transformations. Finally, I present QSynth, a quantum program synthesis framework that synthesizes verified recursive quantum programs, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes 10 quantum unitary programs including quantum arithmetic programs, quantum eigenvalue inversion, quantum teleportation and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.

Thesis (MSc) -- Stellenbosch University, 2003. / ENGLISH ABSTRACT: Software testing tools simplify and automate the menial work associated with testing. Moreover, for complex concurrent software such as computer protocols, testing tools allow testing on an abstract level that is independent of specific implementations. Standard conformance testing methodologies and a number of testing tools are commercially available, but detailed descriptions of the implementation of such testing tools are not widely available. This thesis investigates the development of a tool for automated protocol testing in the ETH Oberon development environment. The need to develop a protocol testing tool that automates the execution of specified test cases was identified in collaboration with a local company that develops protocols in the programming language Oberon. Oberon is a strongly typed secure language that supports modularisation and promotes a readable programming style. The required tool should translate specified test cases into executable test code supported by a runtime environment. A test case consists of a sequence of input actions to which the software under test is expected to respond by executing observable output actions. A number of issues are considered of which the first is concerned with the representation of test case specifications. For this, a notation was used that is basically a subset of the test specification language TTCN-3 as standardised by the European Telecommunications Standards Institute. The second issue is the format of executable test cases and a suitable runtime environment. A translator was developed that generates executable Oberon code from specified test cases. The compiled test code is supported by a runtime library, which is part of the tool. Due to the concurrent nature of a protocol environment, concurrent processes in the runtime environment are identified. Since ETH Oberon supports multitasking in a limited sense, test cases are executed as cooperating background tasks. The third issue is concerned with the interaction between an executing test case and a system under test. It is addressed by an implementation dependent interface that maps specified test interactions onto real interactions as required by the test context in which an implementation under test operates. A supporting protocol to access the service boundary of an implementation under test remotely and underlying protocol service providers are part of a test context. The ETH Oberon system provides a platform that simplifies the implementation of protocol test systems, due to its size and simple task mechanism. Operating system functionality considered as essential is pointed out in general terms since other systems could be used to support such testing tools. In conclusion, directions for future work are proposed. / AFRIKAANSE OPSOMMING: Toetsstelsels vir programmatuur vereenvoudig en outomatiseer die slaafse werk wat met toetsing assosieer word. 'n Toetsstelsel laat verder toe dat komplekse gelyklopende programmatuur, soos rekenaarprotokolle, op 'n abstrakte vlak getoets word, wat onafhanklik van spesifieke implementasies is. Daar bestaan standaard metodes vir konformeringstoetsing en 'n aantal toetsstelsels is kommersiëel beskikbaar. Uitvoerige beskrywings van die implementering van sulke stelsels is egter nie algemeen beskikbaar nie. Hierdie tesis ondersoek die ontwikkeling van 'n stelsel vir outomatiese toetsing van protokolle in die ontwikkelingsomgewing van ETH Oberon. Die behoefte om 'n protokoltoetsstelsel te ontwikkel, wat die uitvoering van gespesifiseerde toetsgevalle outomatiseer, is geïdentifiseer in oorleg met 'n plaaslike maatskappy wat protokolle ontwikkel in die Oberon programmeertaal. Oberon is 'n sterkgetipeerde taal wat modularisering ondersteun en a leesbare programmeerstyl bevorder. Die toestsstelsel moet gespesifiseerde toetsgevalle vertaal na uitvoerbare toetskode wat ondersteun word deur 'n looptydomgewing. 'n Toetsgeval bestaan uit 'n reeks van toevoeraksies waarop verwag word dat die programmatuur wat getoets word, sal reageer deur die uitvoering van afvoeraksies wat waargeneem kan word. 'n Aantal kwessies word aangeraak, waarvan die eerste te make het met die voorstelling van die spesifikasie van toetsgevalle. Hiervoor is 'n notasie gebruik wat in wese 'n subversameling van die toetsspesifikasietaal TTCN-3 is. TTCN-3 is gestandardiseer deur die European Telecommunications Standards Institute. Die tweede kwessie is die formaat van uitvoerbare toetsgevalle en 'n geskikte looptydomgewing. 'n Vertaler is ontwikkel wat uitvoerbare Oberon-kode genereer vanaf gespesifiseerde toetsgevalle. Die vertaalde toetskode word ondersteun deur 'n biblioteek van looptydfunksies, wat deel van die stelsel is. As gevolg van die eienskap dat 'n protokolomgewing uit gelyklopende prosesse bestaan, word daar verskillende tipes van gelyklopende prosesse in 'n protokoltoetsstelsel geïdentifiseer. Aangesien ETH Oberon 'n beperkte multitaakstelsel is, word toetsgevalle vertaal na eindige outomate wat uitgevoer word as samewerkende agtergrondtake. Die derde kwessie het te make met die interaksie tussen 'n toetsgeval wat uitgevoer word en die stelsel wat getoets word. Dit word aangespreek deur 'n koppelvlak wat gespesifiseerde interaksies afbeeld op werklike interaksies soos vereis deur die konteks waarin 'n implementasie onderworpe aan toetsing uitvoer. 'n Ondersteunende protokolom die dienskoppelvlak van die implementasie oor 'n afstand te bereik en ander onderliggende protokoldienste is deel van 'n toetskonteks. Die ETH Oberon-stelsel help in die vereenvoudiging van die implementasie van protokol toetsstelsels, as gevolg van die stelsel se grootte en die eenvoudige taakhanteerder . Die essensiële funksionaliteit van bedryfsstelsels word uitgelig in algemene terme omdat ander stelsels gebruik kan word om toetsstelsels te ondersteun. Ten slotte word voorstelle vir opvolgwerk gemaak.

As organizações necessitam gerenciar informações para obter a melhoria contínua dos seus processos de negócios e agregar conhecimento que ofereça suporte ao processo decisório. Estas informações, muitas vezes, são disponibilizadas por ambientes de Data Warehouse (DW), nos quais os dados são manipulados e transformados. A qualidade dos dados nesses ambientes é essencial para a correta tomada de decisão, tornando-se imprescindível a aplicação de testes. O objetivo deste trabalho é elaborar e validar a aplicação de uma abordagem de teste para DW com o emprego de critérios da técnica de teste baseado em defeitos. A aplicação da abordagem possibilitou testar três fases de desenvolvimento do DW, nas quais estão as Fontes de Dados, processo ETL (Extraction, Transformation and Load) e dados do DW. O critério de teste Análise de Mutantes foi aplicado ao processo ETL por meio de operadores de mutação SQL e a Análise de Instâncias de Dados Alternativas foi aplicada nas fontes de dados e nos dados do DW por meio de classes de defeito nos dados. Essas classes foram geradas por meio da análise e associação dos problemas de qualidade de dados nas fases de desenvolvimento do DW. Os resultados obtidos em estudos de caso permitiram a validação da aplicabilidade e eficácia da técnica de teste baseado em defeitos para ambientes de DW, possibilitando assim revelar quais defeitos podem ocorrer na geração do DW que poderiam prejudicar a qualidade dos dados armazenados nesses ambientes. / Organizations need to manage information for a continuous improvement of its business processes and aggregate knowledge that help in the decision-making process. This information often is provided by Data Warehouse environments (DW), in which data are handled and processed. The quality of data in these environments is essential to make correct decisions, becoming it necessary the application of tests. The objective of this work is to develop and validate the implementation of a testing approach for DW using criteria of Fault-based Testing techniques. The application of the approach enabled tests in three phases of development of the DW, which are the data sources, ETL and DW data. The test criteria Mutation Analysis was applied to the ETL process (Extraction, Transformation and Load) through SQL mutation operators and the Alternative Data Instances Analysis was applied to the data sources and DW data through fault classes on the data. These classes were generated by analyzing and associating of data quality problems in the DW development stages. The results obtained through the case studies allowed assessment of the applicability and effectiveness of testing technique fault for DW environments, thus enabling to reveal faults, which may occur in the generation of DW that could harm the quality of the data stored in these environments.

Contexto: Estudantes de cursos da área de Ciência da Computação que estão iniciando em programação normalmente têm dificuldade de assimilar os conteúdos básicos. Alguns pesquisadores propõem a utilização do desenvolvimento baseado em testes (TDD) a fim de melhorar o ensino, mas sem o foco na qualidade do conjunto de casos de teste. Objetivo: Este trabalho tem o objetivo de propor uma estratégia baseada no desenvolvimento baseado por testes em conjunto com técnicas de teste de software, guiando o aluno a desempenhar suas atividades de programação com mais qualidade e, desta forma, obter melhores resultados acadêmicos. Método: Baseado em um mapeamento sistemático da literatura e na revisão de estudos que aplicam desenvolvimento baseado em testes (TDD) em âmbito educacional, foi definida uma estratégia para integrar critérios de teste ao TDD. Para avaliar os resultados, foram definidas medidas e instrumentos para a coleta de resultados. Foi executado um experimento científico com o público alvo para a obtenção das informações com a finalidade de avaliar a hipótese definida. Resultados: Foi definida uma estratégia de utilização de técnicas de teste de software em conjunto com o TDD para alunos que estão iniciando em programação em cursos de Computação. A estratégia consiste na melhoria do conjunto de casos de teste durante a refatoração no TDD, considerando critérios estruturais baseado em fluxo de controle. Além disso, foram elaboradas ferramentas para a coleta de dados durante o desenvolvimento de programas e para análise dos dados. A estratégia permitiu a melhora do programa e dos casos de teste e foi avaliada pelos estudantes como um guia no desenvolvimento dos casos de teste e como um atalho para descoberta de defeitos. Conclusões: Com a utilização da estratégia proposta, foi possível observar melhorias no conjunto de casos de teste e no software final. A estratégia definida pode ser replicada em outros contextos e com o emprego de outras técnicas e critérios de teste de software para a avaliação da hipótese definida e generalização dos resultados. / Background: Students of Computer Science courses usually have difficulty assimilating the basic contents of introductory programming disciplines. Some researchers propose the use of Test-Driven Development (TDD) to improve teaching, but with no focus in the test set quality. Objective: The goal of this study is to define a strategy for test-driven development using software testing criteria, guiding students to improve the quality of their programming activities, and, consequently, academic results. Method: Initially, we performed a systematic mapping study on TDD in the Computing education context, and a literature review about the usage of test criteria with TDD. Considering the evidences collected, we defined a strategy to integrate the usage of test criteria into TDD. In order to evaluate this strategy, we defined measurements and instruments for data collection. An experimental study was conducted with students to evaluate the strategy and the objective satisfaction. Results: We defined a strategy to use software testing criteria with TDD for students that are learning how to program in Computing courses. The strategy consists into improving the test set while refactoring the code at TDD, considering control-flow-based structural testing criteria. Morever, we developed a set of tools to gather and analyze data produced by the students while using the strategy in the experimental study. The strategy lead to higher quality programs and test sets, and it was considered useful by the students, providing a guide for the creation of test cases, and helping them to discover errors. Conclusions: It was possible to observe improvements into the quality of programs and of test sets. The strategy can be replicated, considering different contexts and evaluting more testing criteria, fostering further evaluation of the objective and generalization of the results.